Publication

Generic Interacting State Machines and their instantiation with dynamic features

Proceedings of ICFEM 2003

Author: David von Oheimb, Volkmar Lotz
Year: 2003
Publisher: Springer
CR Classification: D.2.4, F.1.2, H.2.0
CR General Terms: Security, Reliability, Theory, Verification
Abstract: Interacting State Machines (ISMs) are used to model reactive systems and to express and verify their properties. They can be seen both as automata exchanging messages simultaneously on multiple buffered ports and as communicating processes with explicit local state. We introduce generic ISMs, extending the ISM formalism with global state. We give a typical instantiation, namely support for dynamically changing communication. Other instantiations, e.g. an implemention of boxed mobile ambients, can be used alternatively or in combination, which demonstrates the flexibility of the framework. As an application example we model a simple multi-threaded client/server system. ISMs and all their derivations are formally defined within the theorem prover Isabelle/HOL. The development, textual documentation, and verification of their applications is supported by Isabelle as well, and graphical design and documentation is available via the CASE tool AutoFocus. The conventional state-based approach, its expressiveness and flexibility, and freely available multi-level tool support makes our framework well-suited for practical formal system analysis even in an industrial setting.

BibTeX entry:

@inproceedings{GenISMs03, author = {Oheimb, David von and Volkmar Lotz}, title = {{Generic Interacting State Machines} and their instantiation with dynamic features}, booktitle = {Formal Methods and Software Engineering (ICFEM)}, conference = {5th International Conference on Formal Engineering Methods}, editor = {Jin Song Dong and Jim Woodcock}, publisher = {Springer}, series = {LNCS}, volume = {2885}, pages = {144--166}, month = Nov, year = 2003, note = {\url{http://ddvo.net/papers/GenISMs.html}}, CRClassification = {D.2.4, F.1.2, H.2.0}, CRGenTerms = {Security, Reliability, Theory, Verification}, abstract = { Interacting State Machines (ISMs) are used to model reactive systems and to express and verify their properties. They can be seen both as automata exchanging messages simultaneously on multiple buffered ports and as communicating processes with explicit local state. We introduce generic ISMs, extending the ISM formalism with global state. We give a typical instantiation, namely support for dynamically changing communication. Other instantiations, e.g.\ an implemention of boxed mobile ambients, can be used alternatively or in combination, which demonstrates the flexibility of the framework. As an application example we model a simple multi-threaded client/server system. ISMs and all their derivations are formally defined within the theorem prover Isabelle/HOL. The development, textual documentation, and verification of their applications is supported by Isabelle as well, and graphical design and documentation is available via the CASE tool AutoFocus. The conventional state-based approach, its expressiveness and flexibility, and freely available multi-level tool support makes our framework well-suited for practical formal system analysis even in an industrial setting. } }