Back to Search
Start Over
Symbolic Refinement of Extended State Machines with Applications to the Automatic Derivation of Sub-Components and Controllers
- Source :
- IEEE Transactions on Software Engineering. 47:1-16
- Publication Year :
- 2021
- Publisher :
- Institute of Electrical and Electronics Engineers (IEEE), 2021.
-
Abstract
- Nowadays, extended state machines are prominent requirements specification techniques due to their capabilities of modeling complex systems in a compact way. These machines extend the standard state machines with variables and have transitions guarded by enabling predicates and may include variable update statements. Given a system modeled as an extended state machine, with possibly infinite state space and some non-controllable (parameterized) interactions, a pruning procedure is proposed to symbolically derive a maximal sub-machine of the original system that satisfies certain conditions; namely, some safeness and absence of undesirable deadlocks which could be produced during pruning. In addition, the user may specify, as predicates associated with states, some general goal assertions that should be preserved in the obtained sub-machine. Further, one may also specify some specific requirements such as the elimination of certain undesirable deadlocks at states, or fail states that should never be reached. Application examples are given considering deadlock avoidance and loops including infinite loops over non-controllable interactions showing that the procedure may not terminate. In addition, the procedure is applied for finding a controller of a system to be controlled. The approach generalizes existing work in respect to the considered extended machine model and the possibility of user defined control objectives written as assertions at states.
- Subjects :
- Theoretical computer science
Finite-state machine
Computer science
Software requirements specification
020207 software engineering
02 engineering and technology
Deadlock
Infinite loop
Formal specification
0202 electrical engineering, electronic engineering, information engineering
State space
Pruning (decision trees)
Formal verification
Software
Subjects
Details
- ISSN :
- 23263881 and 00985589
- Volume :
- 47
- Database :
- OpenAIRE
- Journal :
- IEEE Transactions on Software Engineering
- Accession number :
- edsair.doi...........01db950b42b98bf80a1c054fc12fdf5c