Sciweavers

Share
ICFEM
2003
Springer

Generic Interacting State Machines and Their Instantiation with Dynamic Features

10 years 1 months ago
Generic Interacting State Machines and Their Instantiation with Dynamic Features
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 implementation 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 ap...
David von Oheimb, Volkmar Lotz
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where ICFEM
Authors David von Oheimb, Volkmar Lotz
Comments (0)
books