| 1. |
- Miremadi, Sajed, 1983, et al.
(författare)
-
Symbolic Reduction of Guards in Supervisory Control Using Genetic Algorithms
- 2012
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In the supervisory control theory, a supervisor isgenerated based on given plant and specification models. Thesupervisor restricts the plant in order to fulfill the specifications. A problem that is typically encountered in industrial applications is that the resulting supervisor is not easily comprehensible for the users. To tackle this problem, we previously introduced an efficient method to characterize a supervisor by logic conditions, referred to as guards, generated from the models. The guards express under which conditions an event is allowed to occur tofulfill the specifications. By exploiting the structure of the given models, some techniques were introduced to simplify the guards and make them tractable. In order to be able to handle complex systems efficiently, the models are symbolically represented by binary decision diagrams and thus all computations are performed symbolically as well. As a consequence, the size of the guards becomes very sensitive to the variable ordering in the BDDs. In this paper, by using genetic algorithms, we aim to find the optimal variable ordering for the BDDs that yields the most compactguard. The approach has been implemented in a supervisorycontrol tool and applied to an academic example example.
|
|
| 2. |
- Shoaei, Mohammad Reza, 1983, et al.
(författare)
-
Automatic Generation of Controllers for Collision-Free Flexible Manufacturing Systems
- 2010
-
Ingår i: 6th annual IEEE International Conference on Automation Science and Engineering. - 9781424454471 ; , s. 368-373
-
Konferensbidrag (refereegranskat)abstract
- A method for automatic generation of non-blockingcontrollers that generate collision-free flexible manufacturing cells is presented in this paper. Today, industry demands on flexible production sometimes require significant changes in location, orientation and configuration of industrial robots and other moving devices, when new products are introduced. All these changes pose a threat to the devices to collide while sharing workspace. To avoid this, a formal model of the operations in a manufacturing system is generated, and for each operation state a corresponding 3D simulation shape is created. A collision-free system is then achieved by considering pairs of colliding shapes as forbidden states. The automatic generation also includes a synthesis procedure, where a non-blocking and controllable supervisor is generated based on guard generation. The guards are computed by binary decision diagrams, which means that complex systems can be handled, still generating comprehensible restrictions that are easily included in PLC-code.
|
|
| 3. |
- Shoaei, Mohammad Reza, 1983, et al.
(författare)
-
Reduced-order synthesis of operation sequences
- 2011
-
Ingår i: IEEE International Conference on Emerging Technologies and Factory Automation, ETFA. - 1946-0759 .- 1946-0740. - 9781457700170 ; , s. 8-
-
Konferensbidrag (refereegranskat)abstract
- In flexible manufacturing systems a large number of operations need to be coordinated and supervised to avoid blocking and deadlock situations. The synthesis of such supervisors soon becomes unmanageable for industrial manufacturing systems, due to state space explosion. In this paper we therefore develop some reduction principles for a recently presented model based on self-contained operations and sequences of operations. First sequential operation behaviors are identified and related operation models are simplified into one model. Then local transitions without interaction with other operation models are removed. This reduction principle is applied to a synthesis of non-blocking operation sequences, where collisions among moving devices are guaranteed to be avoided by a flexible booking process. The number of states in the synthesis procedure and the computation time is reduced dramatically by the suggested reduction principle.
|
|
| 4. |
- Bengtsson, Kristofer, 1979, et al.
(författare)
-
Relations Identification and Visualization for Sequence Planning and Automation Design
- 2010
-
Ingår i: In Proc. IEEE Conference on Automation Science and Engineering, Toronto. - 9781424454471 ; , s. 841 - 848
-
Konferensbidrag (refereegranskat)abstract
- The sequential behavior of a manufacturing system results from a number of constraints introduced both in product, manufacturing and control logic development. Sequence planning is therefore an important activity throughout the complete development process. This paper proposes a sequence planning approach using self-contained manufacturing operations that model actions and relevant execution conditions. These operations can have temporal relations with each other, due to execution constraints expressed by operation pre- post- and reset conditions. The operation relations can for example be parallel, sequence, arbitrary order, alternative or hierarchy. Based on a formal operation model, the relations among operations are identified and visualized with a graphical language called Sequences of Operations, SOP.
|
|
| 5. |
- Bengtsson, Kristofer, 1979, et al.
(författare)
-
Sequence Planning Using Multiple and Coordinated Sequences of Operations
- 2012
-
Ingår i: IEEE Transactions on Automation Science and Engineering. - 1558-3783 .- 1545-5955. ; 9:2, s. 308-319
-
Tidskriftsartikel (refereegranskat)abstract
- The sequential behavior of a manufacturing system results from several constraints introduced during the product, manufacturing, and control logic development. This paper proposes methods and algorithms for automatically representing and visualizing this behavior from various perspectives throughout the development process. A new sequence planning approach is introduced that uses self-contained operations to model the activities and execution constraints. These operations can be represented and visualized from multiple perspectives using a graphical and formal language called Sequences of Operations (SOPs). The operations in a manufacturing system are related to each other in various ways, due to execution constraints expressed by operation pre- and post-conditions. These operation relations include parallel, sequence, arbitrary order, alternative, and hierarchy relations. Based on the SOP language, these relations are identified and visualized in various SOPs and sequences. A software tool, Sequence Planner, has been developed, for organizing the operations into SOPs that visualize only relevant operations and relations. Note to Practitioners-This paper proposes methods and algorithms for a new sequence planning approach in which sequences are automatically created based on the relations among operations instead of having to be manually constructed. Using various views, the sequences of operations related to, for example, part flow, robot operations, and operator tasks, can be visualized. The use of various views helps the user better understand the relations between cell control and mechanical design, and between product design and total system behavior.
|
|
| 6. |
- Claessen, Koen, 1975, et al.
(författare)
-
Applying valued booleans in testing of cyber-physical systems
- 2018
-
Ingår i: Proceedings - 2018 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT-CPS 2018. ; , s. 8-9
-
Konferensbidrag (refereegranskat)abstract
- In software testing, as in cyber-physical systems testing, test suites are traditionally developed by hand. In this work we consider one framework for putting the computer in charge of the testing instead: constrained random test case generation as supported by the tool QuickCheck. This is implemented by the use of Valued Booleans (VBools). VBools naturally allow for an extension of QuickCheck into cyber-physical systems, which is useful particularly since QuickCheck can perform shrinking of test cases. Shrinking is a technique to make test cases simpler while preserving failure.
|
|
| 7. |
- Eddeland, Johan, 1991, et al.
(författare)
-
Automated Mode Coverage Analysis for Cyber-Physical Systems using Hybrid Automata
- 2017
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 50:1, s. 9260-9265
-
Konferensbidrag (refereegranskat)abstract
- Testing of cyber-physical systems (CPSs) is a complex task, mainly due to the presence of continuous dynamics. In industry, CPSs are typically safety-critical and their complexity is rapidly increasing. Thus, it is important to know how well the tests perform. One common approach to ensuring test quality is to use coverage criteria, for example the well-known MC/DC. However, most of the used coverage criteria in industry depend on code structure to find errors in the system and may fail to capture the complete dynamical behaviour. Two coverage definitions are presented that can be used to ensure that all the continuous dynamics in the system have been explored. It is shown that the MC/DC criterion is not always rigorous enough to test all the system behaviour. Finally, the proposed coverage criteria are applied to automatically assess the test quality for a plant model used at Volvo Car Corporation.
|
|
| 8. |
- Eddeland, Johan, 1991, et al.
(författare)
-
Objective functions for falsification of signal temporal logic properties in cyber-physical systems
- 2017
-
Ingår i: IEEE International Conference on Automation Science and Engineering. - 2161-8070 .- 2161-8089. - 9781509067817 ; 2017-August, s. 1326-1331
-
Konferensbidrag (refereegranskat)abstract
- Cyber-physical systems, such as automation and automotive systems, are highly complex systems that are frequently also safety-critical. Thus, it is important that these systems behave as intended, as incorrectness can have serious consequences. Due to continuous dynamics that yield infinite state spaces, the systems cannot be exhaustively tested to guarantee correct behavior, but systematic testing can be used to systematically search for behavior that is inconsistent with the requirements. However, manual testing is a tedious and error-prone task, and thus it is desirable to automate as much of the testing process as possible to increase efficiency and eliminate manual errors. This paper considers falsification of requirements expressed as temporal logic formulae to find errors in the Model-in-the-Loop stage of model-based development. The falsification is an optimization procedure where the objective function is determined by the definition of a quantitative semantics for the temporal logic formalism, and the optimization is performed over an input parametrization. It is shown that in certain cases where the discreteness of the system under test manifests itself in the objective function, the robustness values for the temporal logic specifications need to be modified. This paper presents two alternative objective functions suitable for these cases, and illustrates their use with both a small example and a use case from Volvo Car Corporation.
|
|
| 9. |
- Fabian, Martin, 1960, et al.
(författare)
-
Supervisory control of manufacturing systems using extended finite automata
- 2014
-
Ingår i: Formal Methods in Manufacturing. - 9781466561564 ; , s. 295-314
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- Discrete event systems (DES) are typically man-made reactive systems such as manufacturing, traffic control and embedded systems. DES behaviours are modelled in terms of states and events; states represent certain situations under which specific properties hold, while events represent significant occurrences that change those properties. A DES occupies at each time instant a single state out of its many possible ones and transits to another state on the occurrence of an event. One typical modelling formalism for DES is finite automata (FA) [1] that explicitly represent the states and the transitions between them.
|
|
| 10. |
- Fei, Zhennan, 1984, et al.
(författare)
-
A BDD-Based Approach for Designing Maximally Permissive Deadlock Avoidance Policies for Complex Resource Allocation Systems
- 2015
-
Ingår i: IEEE Transactions on Automation Science and Engineering. - 1558-3783 .- 1545-5955. ; 12:3, s. 990-1006
-
Tidskriftsartikel (refereegranskat)abstract
- In order to develop a computationally efficient implementation of the maximally permissive deadlock avoidance policy (DAP) for complex resource allocation systems (RAS), a recent approach focuses on the identification of a set of critical states of the underlying RAS state-space, referred to as minimal boundary unsafe states. The availability of this information enables an expedient one-step-lookahead scheme that prevents the RAS from reaching outside its safe region. The work presented in this paper seeks to develop a symbolic approach, based on binary decision diagrams (BDDs), for efficiently retrieving the (minimal) boundary unsafe states from the underlying RAS state-space. The presented results clearly demonstrate that symbolic computation enables the deployment of the maximally permissive DAP for complex RAS with very large structure and state-spaces with limited time and memory requirements. Furthermore, the involved computational costs are substantially reduced through the pertinent exploitation of the special structure that exists in the considered problem.
|
|
