Interactive Verification of UML State Machines

Simon Bäumler, Michael Balser, Alexander Knapp, Wolfgang Reif, Andreas Thums

Interactive Verification of UML State Machines

We propose a new technique for interactive formal verification of temporal properties of UML state machines. We introduce a formal, operational semantics of UML state machines and give an overview of the proof method which is based on symbolic execution with induction. Usefulness of the approach is demonstrated by example of an automatic teller machine. The approach is implemented in the KIV system.
published 2004 6th International Conference on Formal Engineering Methods, ICFEM 2004, Proceedings, Lecture Notes in Computer Science, volume 3308

Publisher: Springer LNCS 3308

ISBN: 3-540-23841-7