| 1. |
- Fabian, Martin, 1960, et al.
(författare)
-
Lupremica - Lua Scripting for Supremica
- 2023
-
Ingår i: IFAC-PapersOnLine. - 2405-8963. ; 56:2, s. 6099-6104
-
Konferensbidrag (refereegranskat)abstract
- Supremica is a software tool that implements several state-of-the-art algorithms to manipulate discrete-event systems, such as different types of compositions and compositional supervisor synthesis. Lua is a light-weight programming language suitable as a scripting language embedded into other applications. This paper describes the use of Lua as a scripting language for Supremica. To this end, the LuaJ interpreter is added to Supremica as a bridge between the Java-based implementation of Supremica and the Lua scripts. In this way, Supremica's entire Java API is made available to Lua scripts. Thus, scripts can automatically create automata, and manipulate them with all the algorithms available in Supremica and further manipulate the result with new algorithms implemented by Lua scripts. This opens up a new world of possibilities to try out new ideas and to extend the power of Supremica.
|
|
| 2. |
- Khan, Adnan, 1984, et al.
(författare)
-
On test case reduction for testing safety properties of manufacturing systems
- 2022
-
Ingår i: Journal of Manufacturing Systems. - : Elsevier BV. - 0278-6125. ; 63, s. 203-213
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents an approach to reduce the number of test cases, and hence testing time for the safe input-output conformance simulation relation (safe-IOCOS). The safe-IOCOS relation requires the implementation to be trace equivalent with respect to the specification only for traces composed of safety behaviors, which makes safe-IOCOS a suitable relation to test safety properties in practical settings. However, in typical manufacturing systems, multiple safety behaviors are typically associated with each nominal operation in the implementation. Thus, if safe-IOCOS is used industrially then testing for safety related faults becomes time consuming as the traces composed of same safety behaviors gets tested multiple times. This is possible either if the target states reached after the execution of traces have the same past behavior or the same future behavior. To remedy this, two reduction methods are proposed in this paper, subset construction and bisimulation equivalence. Both reduction methods preserve the traces of the system. Using both subset construction and bisimulation, a given specification can be maximally reduced and then used to implement the manufacturing system. The implementation based on a maximally reduced bisimilar specification allows the test engineer to omit test cases if the same safety behavior has already been tested. Furthermore, faults related to missing safety behaviors that are associated with multiple traces can be uncovered more efficiently compared to if the non-reduced specification is used for testing. To summarize, testing is a laborious problem, which can benefit from methods that enable reduction in testing time and makes the testing procedure efficient in terms of uncovering errors.
|
|
| 3. |
- Krook, Jonas, 1986, et al.
(författare)
-
Modeling and Synthesis of the Lane Change Function of an Autonomous Vehicle
- 2018
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 51:7, s. 133-138
-
Konferensbidrag (refereegranskat)abstract
- Unexpected incorrect behavior of autonomous vehicles can have catastrophic outcomes. But, as with any large-scale software development, correctness of the system is not easily guaranteed. As the system is made up of multiple sub-modules that interact with each other, unexpected behavior can arise from incorrect interactions between the modules. In a previous paper, formal verification was applied to the lane change module of the decision and control software (under development) for an autonomous vehicle. This revealed incorrectness in the model, which could also be shown to exist in the actual software. Manual changes to the model did not result in absence of the incorrectness, and so in this paper we aim to patch the error by applying synthesis. The synthesized result is correct by construction, but it is not obvious what part of the functionality is disabled by the synthesis. Though different synthesis techniques were able to generate supervisors for the model, only when the supervisor was expressed as guard conditions on the events was it possible to interpret the effect of the synthesis. However, the supervisors put constraints on how the input data to the lane change module might change, so in the end the supervisors put behavioral requirements on the modules that generate the input to the lane change module.
|
|
| 4. |
- Krook, Jonas, 1986, et al.
(författare)
-
Robust Stutter Bisimulation for Abstraction and Controller Synthesis with Disturbance: Proofs
- 2022
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- This paper proposes a method to synthesise controllers for cyber-physical systems such that the controlled systems satisfy specifications given as linear temporal logic formulas. The focus is on systems with disturbance, where future states cannot be predicted exactly due to uncertainty in the environment. The approach used to solve this problem is to first construct a finite-state abstraction of the original system and then synthesise a controller for the abstract system. For this approach, the robust stutter bisimulation relation is introduced, which preserves the existence of controllers for any given linear temporal logic formula. States are related by the robust stutter bisimulation relation if the same target sets can be guaranteed to be reached or avoided under control of some controllers, thereby ensuring that disturbances have similar effect on paths that start in related states. This paper presents an algorithm to construct the corresponding robust stutter bisimulation quotient to solve the abstraction problem, and it is shown, by explicit construction, that there exists a controller enforcing a linear temporal logic formula for the original system if and only if a corresponding controller exists for the quotient system. Lastly, the result of the algorithm and the controller construction are demonstrated by application to an example of robot navigation.
|
|
| 5. |
- 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.
|
|
| 6. |
- 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.
|
|
| 7. |
- Mohajerani, Sahar, 1982, et al.
(författare)
-
A Framework for Compositional Synthesis of Modular Nonblocking Supervisors
- 2014
-
Ingår i: IEEE Transactions on Automatic Control. - 0018-9286 .- 1558-2523. ; 59:1, s. 150-162
-
Tidskriftsartikel (refereegranskat)abstract
- This paper describes a framework for compositional supervisor synthesis, which is applicable to all discrete event systems modeled as a set of deterministic automata. Compositional synthesis exploits the modular structure of the input model, and therefore works best for models consisting of a large number of small automata. The state-space explosion is mitigated by the use of abstraction to simplify individual components, and the property of synthesis equivalence guarantees that the final synthesis result is the same as it would have been for the non-abstracted model. The paper describes synthesis equivalent abstractions and shows their use in an algorithm to efficiently compute supervisors. The algorithm has been implemented in the DES software tool Supremica and successfully computes nonblocking modular supervisors, even for systems with more than 10(14) reachable states, in less than 30 seconds.
|
|
| 8. |
- Mohajerani, Sahar, 1982, et al.
(författare)
-
An algorithm for compositional nonblocking verification of extended finite-state machines
- 2014
-
Ingår i: IFAC Proceedings Volumes (IFAC-PapersOnline). - 2405-8963. ; 47:2, s. 376-382
-
Konferensbidrag (refereegranskat)abstract
- This paper describes an approach for compositional nonblocking verification of discrete event systems modelled as extended finite-state machines (EFSM). Previous results about finite-state machines in lock-step synchronisation are generalised and applied to EFSMs communicating via shared variables. This gives rise to an EFSM-based conflict check algorithm that composes EFSMs gradually and partially unfolds variables as needed. At each step, components are simplified using conflict-equivalence preserving abstraction. The algorithm has been implemented in the discrete event systems tool Supremica. The paper presents experimental results for the verification of two scalable manufacturing system models, and shows that the EFSM-based algorithm verifies some large models faster than previously used methods.
|
|
| 9. |
- Mohajerani, Sahar, 1982, et al.
(författare)
-
An Algorithm for Weak Synthesis Observation Equivalence for Compositional Supervisor Synthesis
- 2012
-
Ingår i: IFAC Proceedings Volumes (IFAC-PapersOnline). - 2405-8963. ; 239--244
-
Konferensbidrag (refereegranskat)abstract
- This paper proposes an algorithm to simplify automata in such a way that compositional synthesis results are preserved in every possible context. It relaxes some requirements of synthesis observation equivalence from previous work, so that better abstractions can be obtained. The paper describes the algorithm, adapted from known bisimulation equivalence algorithms, for the improved abstraction method. The algorithm has been implemented in the DES software tool Supremica and has been used tocompute modular supervisors for several large benchmark examples. It successfully computes modular supervisors for systems with more than 10^12 reachable states.
|
|
| 10. |
- Mohajerani, Sahar, 1982, et al.
(författare)
-
Compositional and Abstraction-Based Approach for Synthesis of Edit Functions for Opacity Enforcement
- 2019
-
Ingår i: IEEE Transactions on Automatic Control. - 0018-9286 .- 1558-2523. ; 65:8, s. 3349 -3364
-
Tidskriftsartikel (refereegranskat)abstract
- This article develops a novel compositional and abstraction-based approach to synthesize edit functions for opacity enforcement in modular discrete event systems. Edit functions alter the output of the system by erasing or inserting events in order to obfuscate the outside intruder, whose goal is to infer the secrets of the system from its observation. We synthesize edit functions to solve the opacity enforcement problem in a modular setting, which significantly reduces the computational complexity compared with the monolithic approach. Two abstraction methods called opaque observation equivalence and opaque bisimulation are first employed to abstract the individual components of the modular system and their observers. Subsequently, we propose a method to transform the synthesis of edit functions to the calculation of modular supremal nonblocking supervisors. We show that the edit functions synthesized in this manner correctly solve the opacity enforcement problem.
|
|
