| 1. |
|
|
| 2. |
- Byröd, Martin, 1980, et al.
(author)
-
Efficient Reachability Analysis on Modular Discrete-Event Systems using Binary Decision Diagrams
- 2006
-
In: 8th International Workshop on Discrete Event Systems, WODES 2006; Ann Arbor, MI; United States; 10 July 2006 through 12 July 2006. - 1424400538 ; , s. 288-293
-
Conference paper (peer-reviewed)abstract
- A well known strategy for handling the exponential complexity of modular discrete event systems is to represent the state space symbolically, using binary decision diagrams (BBDs). In this paper, key success factors in the design of efficient BDD-based reachability algorithms for synthesis and verification are discussed. It is also shown how the modular structure of a discrete event system (DES) can be utilized by taking advantage of the process communication graph and partitioning techniques. A reachability algorithm based on these principles is discussed and a proof of correctness for the algorithm is given.
|
|
| 3. |
- Cengic, Goran, 1978, et al.
(author)
-
A Control Software Development Method Using IEC 61499 Function Blocks, Simulation and Formal Verification
- 2008
-
In: Proceedings of the 17th IFAC World Congress. ; , s. 22-27
-
Journal article (peer-reviewed)abstract
- A new control software development method is presented. It uses IEC 61499 function blocks for control software programming and provides tools for simulation, execution, automatic model generation and formal verification of the control code during the development. Simulation and execution are supported by the same tool, the Fuber runtime environment. Formal modeling is done using extended finite automata (EFA) and an automatic model generation tool. Formal verification shows the behavior of the closed-loop system. i.e. when control code is executed against the model of the process. The model can use a non-deterministic execution control chart (ECC) in the process model block. The control code and the process model are expressed using the IEC 61499 language in order to avoid maintenance of the process model and control code in different languages, thus making it easier to use the formal verification in the control software development.
|
|
| 4. |
- Cengic, Goran, 1978, et al.
(author)
-
A Framework for Component Based Distributed Control Software Development Using IEC 61499
- 2006
-
In: Proceedings of the 2006 IEEE International Conference on Emerging Technology and Factory Automation, Sep 2006, Prague, Czech Republic.
-
Journal article (peer-reviewed)abstract
- A framework for component based distributed control software is proposed. The primary application for the framework is in distributed control systems. The framework proposes new software components, called automation components that can be hierarchically embedded to produce new components. Automation components are also combined to produce hierarchical component based applications. The framework is independent of the execution platform, however it is shown how an application that is developed using the framework can be executed using IEC 61499 platform. The validity of the framework is evaluated using an industrial example of a reconfigurable manufacturing cell.
|
|
| 5. |
- Cengic, Goran, 1978, et al.
(author)
-
Definition of the Execution Model Used in the Fuber IEC 61499 Runtime Environment
- 2008
-
In: Proceedings of the 6th IEEE International Conference on Industrial Informatics. - 1935-4576. ; , s. 301-306
-
Journal article (peer-reviewed)abstract
- The buffered sequential execution model (BSEM) for IEC 61499 function block applications is presented. Before the execution of the application the composite function blocks are flattened. The resulting application containing the basic and service interface function blocks is executed. The basic function blocks are put in the ready queue in the same order that they receive the input events, hence the word ldquosequentialrdquo in the name. Each basic function block keeps a queue of incoming events with their associated data, hence the word ldquobufferedrdquo in the name. Scheduling policy of the blocks is in the scheduling function while the execution policy of the received events is in the function block instance. The extended finite automata models suitable for formal verification of the proposed execution modelpsilas behavior are presented. The model may be analyzed using a discrete event systems tool called Supremica. The presented execution model is implemented in the Fuber runtime environment.
|
|
| 6. |
- Cengic, Goran, 1978, et al.
(author)
-
Formal Modeling of Function Block Applications Running in IEC 61499 Execution Runtime
- 2006
-
In: 2006 IEEE Conference on Emerging Technologies and Factory Automation, ETFA; Hamburg; Germany; 20 September 2006 through 22 September 2006. - 9781424406814 ; , s. 1269-1276
-
Conference paper (peer-reviewed)abstract
- The execution model in a new standard for distributed control systems, IEC 61499, is analyzed. It is shown how the same standard compliant application running in two different standard compliant runtime environments may result in completely different behaviors. Thus, to achieve true portability of applications between multiple standard compliant runtime environments a more detailed execution model is necessary. In this paper a new runtime environment, Fuber, is presented along with a formal execution model. In this case the execution model is given as a set of interacting state machines which makes it straightforward to analyze the behavior of the application and runtime together using existing tools for formal verification.
|
|
| 7. |
|
|
| 8. |
- Flordal, Hugo, 1977, et al.
(author)
-
Automatic model generation and PLC-code implementation for interlocking policies in industrial robot cells
- 2007
-
In: Control Engineering Practice. - : Elsevier BV. - 0967-0661. ; 15:11, s. 1416-1426
-
Journal article (peer-reviewed)abstract
- In industrial production lines, for example in the automotive industry, cells with multiple industrial robots are common. In such cells, each robot has to avoid running into static obstacles and when the robots work together in a shared space they must also avoid colliding with each other. Typically. the latter is enforced by manually implementing interlocks in programmable logic controllers (PLCs). This is a tedious. error-prone task that is a bottleneck in the development of production lines. The PLC-code being man-made also greatly complicates the maintenance and reconfiguration of such production lines. However, in industry today, a lot of development of robot cells is made offline in 3D simulation environments which enables the use of computers also for deciding and implementing the necessary coordination. This paper presents a method that makes use of information in a robot simulation environment in order to automatically extract finite state models. These models can be used to generate supervisors for ensuring that the deadlock situations that may arise as a consequence of the introduced interlocks are avoided. It is also possible to optimize the work cycle time for the cell. Finally, PLC-code to supervise the production cell can be automatically generated from the deadlock-free and possibly optimized system model. This approach results in a high flexibility in that the coordination function can be quickly reimplemented whenever necessary. A prototype implementation has been developed making use of a commercial 3D robot simulation tool, and a software tool for supervisor synthesis and code generation. The approach is general and should be possible to implement in most offline robot simulation tools. (c) 2007 Elsevier Ltd. All rights reserved.
|
|
| 9. |
- Flordal, Hugo, 1977, et al.
(author)
-
Compositional Synthesis of Maximally Permissive Supervisors Using Supervision Equivalence
- 2007
-
In: Discrete Event Dynamic Systems: Theory and Applications. - : Springer Science and Business Media LLC. - 0924-6703 .- 1573-7594. ; 17:4, s. 475-504
-
Journal article (peer-reviewed)abstract
- This paper presents a general framework for efficient synthesis of supervisors for discrete event systems. The approach is based on compositional minimisation, using concepts of process equivalence. In this context, a large number of ways are suggested how a finite-state automaton can be simplified such that the results of supervisor synthesis are preserved. The proposed approach yields a compact representation of a least restrictive supervisor that ensures controllability and nonblocking. The method is demonstrated on a simple manufacturing example to significantly reduce the number of states constructed for supervisor synthesis. © 2007 Springer Science+Business Media, LLC.
|
|
| 10. |
|
|
