Paper Info
Title
Institution-based Encoding and Verification of Simple UML State Machines in CASL/SPASS
Abstract
This paper provides the first correct semantical representation of UML state-machines within the logical framework of an institution (previous attempts were flawed). A novel encoding of this representation into first-order logic enables symbolic analyses through a multitude of theorem-provers. UML state-machines are central to model-based systems-engineering. Till now, state-machine analysis has been mostly restricted to model checking, which for state-machines suffers heavily from the state-space explosion problem. Symbolic reasoning, as enabled and demonstrated here, provides a powerful alternative, which can deal with large or even infinite state spaces. Full proofs are given.
Year
DOI
Venue
2020
10.1007/978-3-030-73785-6_7
WADT
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
0
4
Name
Order
Citations
PageRank
Tobias Rosenberger100.34
Saddek Bensalem202.37
Alexander Knapp3162.66
Markus Roggenbach429432.63