| 131. |
- Ljungkrantz, Oscar, 1978, et al.
(författare)
-
Reusable Components for Industrial Logic Control Programming
- 2008
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This paper addresses the problem of developing logic control programs in industry to cope with new requirements of flexible manufacturing systems. We propose a component based approach in which the control program is developed using Reusable Automation Components (RACs). Reusing components may speed up the development and also make the control program have fewer bugs. To get these benefits it is important that components already verified to work properly are reused. The RACs thus contain not only the implementation but may also be richly specified, using concepts from Design by Contract in object-oriented software development. The specification is helpful both for users of the components and for developers since the complete RAC including the specification can be translated to a tool for formal verification, to determine whether the specification is fulfilled or not. The RAC is introduced for general implementation languages and it is in this paper shown in detail how the RAC can be implemented and specified using the common IEC 61131 standard and especially Ladder Diagrams, the most common language today for logic control programs. An example RAC is specified, implemented and finally verified.
|
|
| 132. |
- Ljungkrantz, Oscar, 1978, et al.
(författare)
-
Towards Industrial Formal Specification of Programmable Safety Systems
- 2012
-
Ingår i: IEEE Transactions on Control Systems Technology. - 1063-6536 .- 1558-0865. ; 20:6, s. 1567-1574
-
Tidskriftsartikel (refereegranskat)abstract
- Formal methods for specification and verification are promising in developing PLC (Programmable Logic Controller) programs in manufacturing industry. Particularly this holds for safety PLCs, used to protect humans and equipment from injuries and damages. An important challenge though, is the development of formal specifications, typically a tough task for control engineers. This paper proposes a systematic work procedure that can be used as a first step of developing formal specifications of safety PLC programs in industry. The work procedure intends to facilitate the development of relevant formal properties for safety PLC program components. The formal specifications can be used for automatic formal verification of the components, using model checking techniques. The paper shows how the work procedure has been applied to industrial safety components, resulting in relevant and nontrivial specifications.
|
|
| 133. |
- Magnusson, Patrik, 1984, et al.
(författare)
-
Modular specification of forbidden states for supervisory control
- 2010
-
Ingår i: IFAC Proceedings Volumes. 10th International Workshop on Discrete Event Systems (WODES), Berlin, 30 August - 1 September 2010. - 1474-6670. - 9783902661791 ; 10, s. 412-417
-
Konferensbidrag (refereegranskat)abstract
- A method for solving the forbidden state problem in the Supervisory Control Theory framework is presented. In many real-world applications both the plant and specification is given as a set of interacting automata or processes. In this work, we enable specification of forbidden states within such a modular structure. The aim with the method is to make each forbidden modular state combination uncontrollable. It is then possible to use efficient modular synthesis algorithms for calculation of a modular supervisor where the forbidden states are removed.
|
|
| 134. |
- Magnusson, Patrik, 1984, et al.
(författare)
-
Planning transport sequences for flexible manufacturing systems
- 2011
-
Ingår i: IFAC Proceedings Volumes (IFAC-PapersOnline). - 2405-8963. - 9783902661937 ; 18:PART 1, s. 9494-9499
-
Konferensbidrag (refereegranskat)abstract
- When designing a manufacturing system it is important to plan what the systemshould do. One important activity in most manufacturing systems is to transport products orresources between different positions. In a flexible manufacturing system it can be challengingto design and plan these transport operations due to their complex logical behavior. This paperpresents a method that identifies, creates and visualizes these transport operations based oninputs from a standard virtual manufacturing tool and a high level product operation recipe.The planning of the created transport operations is transformed into a problem of finding anon-blocking solution for a discrete model of the product refinement.
|
|
| 135. |
- Malik, Robi, et al.
(författare)
-
A survey on compositional algorithms for verification and synthesis in supervisory control
- 2023
-
Ingår i: Discrete Event Dynamic Systems: Theory and Applications. - 0924-6703 .- 1573-7594. ; 33:3, s. 279-340
-
Tidskriftsartikel (refereegranskat)abstract
- This survey gives an overview of the current research on compositional algorithms for verification and synthesis of modular systems modelled as interacting finite-state machines. Compositional algorithms operate by repeatedly simplifying individual components of a large system, replacing them by smaller so-called abstractions, while preserving critical properties. In this way, the exponential growth of the state space can be limited, making it possible to analyse much bigger state spaces than possible by standard state space exploration. This paper gives an introduction to the principles underlying compositional methods, followed by a survey of algorithmic solutions from the recent literature that use compositional methods to analyse systems automatically. The focus is on applications in supervisory control of discrete event systems, particularly on methods that verify critical properties or synthesise controllable and nonblocking supervisors.
|
|
| 136. |
- Malik, R., et al.
(författare)
-
Modelling large-scale discrete-event systems using modules, aliases, and extended finite-state automata
- 2011
-
Ingår i: IFAC Proceedings Volumes (IFAC-PapersOnline). - 2405-8963. - 9783902661937 ; 18:PART 1, s. 7000-7005
-
Konferensbidrag (refereegranskat)abstract
- This paper describes the instantiation features currently implemented in the discrete-event systems modelling and analysis tool Supremica. Modules enable users to design reusable groups of related automata and define clear interfaces to describe their interaction. Parametrisation and repetition make it easy to design very large models of regular structure. In combination with its support for extended finite-state automata (EFA), these features enable Supremica users to develop highly complex models of discrete-event systems using a wide variety of modelling styles.
|
|
| 137. |
- Malik, Robi, et al.
(författare)
-
Supremica–An Efficient Tool for Large-Scale Discrete Event Systems
- 2017
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 50:1, s. 5794-5799
-
Konferensbidrag (refereegranskat)abstract
- Supremica is a tool for the modelling and analysis of discrete-event control functions based on state machine models of the uncontrolled plant and specification of the desired closed-loop behaviour. The modelling framework in Supremica is based on finite-state machines extended with variables, guard conditions, and action functions. In order to handle large-scale problems of industrially interesting size, Supremica uses advanced model checking techniques such as symbolic representations and compositional abstraction. Supremica has been used in several industrial research projects to verify and synthesise control functions for embedded controllers, industrial robots, and flexible manufacturing systems, and to verify program code for autonomous vehicles. This paper gives an overview of the modelling features of Supremica, shows the verification and synthesis facilities and their performance for large problems, and presents some of the industrial applications where Supremica has been used.
|
|
| 138. |
- Miremadi, Sajed, 1983, et al.
(författare)
-
Solving Two Supervisory Control Benchmark Problems Using Supremica
- 2008
-
Ingår i: 9th International Workshop on Discrete Event Systems, 2008. - 9781424425921 ; , s. 131-136
-
Konferensbidrag (refereegranskat)abstract
- Two supervisory control benchmark problems for WODES'08 are solved using the tool Supremica. Supremica is a tool for formal synthesis of discrete-event control functions based on discrete event models of the uncontrolled plant and specifications of the desired closed-loop behavior. By using formal synthesis of control functions the need for formal verification is reduced since the control functions are computed to automatically fulfill the given specifications, that is, they are "correct by construction". The modeling framework in Supremica is based on finite automata. Supremica implements several techniques for being able to solve large scale problems. In this paper it is evaluated how the algorithms implemented in Supremica that are based on binary decision diagrams performs on the two benchmark problems. The two benchmark problems are generalization of two classical problems; cat and mouse, and the dining philosophers' problem. The benchmark problems are parametrized such that it is possible to create problem instances with huge state-spaces. The benchmark shows that Supremica can efficiently solve rather large problem instances.
|
|
| 139. |
- Miremadi, Sajed, 1983, et al.
(författare)
-
Supervisor Computation and Representation: A Case Study
- 2010
-
Ingår i: 10th International Workshop on Discrete Event Systems, Berlin; 30 August 2010 through 1 September 2010. - 1474-6670. - 9783902661791 ; 10:1, s. 275-280
-
Konferensbidrag (refereegranskat)abstract
- When supervisory control theory is applied to industrial problems the need for a more expressive modeling formalism than plain event based automata is crucial. The models are typically built in a bottom-up structure where multiple sub-plant and sub-specifications together compose the full plant and specification, respectively. Typically, the enabling of an event in a sub-model may depend on the state of other sub-models. The standard approach is to synchronize on shared events. However, to build models of large industrial problems with complex constraints between sub-models are beyond many engineers abilities. One attempt to deal with this problem is to extend the plain automata with variables and allow guard conditions and action functions to be associated with transitions. This paper discusses the strengths and weaknesses of one such formulation that fits well together with the standard supervisory control theory. A related problem is how to represent the result after the synthesis procedure, i.e., the supervisor. In this paper we present an approach where the supervisor may be represented as extended guard conditions on the original sub-models. This allows an efficient and comprehensible representation of complex supervisors. Hence, it is preferable both from a user, as well as an implementation perspective. Both the modeling formalism based on extended finite automata and the way to represent the supervisor as extended guard conditions have been implemented in a supervisory control tool.
|
|
| 140. |
- Mohajerani, Sahar, 1982, et al.
(författare)
-
A framework for compositional nonblocking verification of extended finite-state machines
- 2016
-
Ingår i: Discrete Event Dynamic Systems: Theory and Applications. - : Springer Science and Business Media LLC. - 0924-6703 .- 1573-7594. ; 26:1, s. 1-52
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents a framework for compositional nonblocking verification of discrete event systems modelled as extended finite-state machines (EFSM). Previous results are improved to consider general conflict-equivalence based abstractions of EFSMs communicating both via shared variables and events. Performance issues resulting from the conversion of EFSM systems to finite-state machine systems are avoided by operating directly on EFSMs, deferring the unfolding of variables into state machines as long as possible. Several additional methods to abstract EFSMs and remove events are also presented. The proposed algorithm has been implemented in the discrete event systems tool Supremica, and the paper presents experimental results for several large EFSM models that can be verified faster than by previously used methods.
|
|
