Interacting State Machines for Mobility

10 years 11 months ago
Interacting State Machines for Mobility
We present two instantiations of generic Interactive State Machines (ISMs) with mobility features which are useful for modeling and verifying dynamically changing mobile systems. ISMs are automata with local state exchanging messages simultaneously on multiple buffered ports. A system of generic ISMs also deals with global state used e.g. to describe their communication topology. We introduce Ambient ISMs (AmbISMs) whose features include hierarchical environments, migration, and locality constraints on communication. In this way we give an alternative operational semantics to the (boxed) ambient calculus. Moreover, we combine AmbISMs with dynamic ISMs which introduce dynamic communication structures and ISM activation and deactivation, as defined in an accompanying paper. All ISM variants have been defined formally within the theorem prover Isabelle/HOL and provide an easy to learn description language for the development, documentation and verification of mobile systems. We motiva...
Thomas A. Kuhn, David von Oheimb
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where FM
Authors Thomas A. Kuhn, David von Oheimb
Comments (0)