Interacting State Machines (ISMs)

Interacting State Machines are a formalism for abstract modeling and verification of reactive systems. ISMs can be seen as high-level variants of Input/Output Automata or as AutoFocus automata with buffered I/O.

ISM structure

ISMs are typically defined graphically using AutoFocus, translated with a converter tool to Isabelle/HOL theory sections, and mechanically verified within Isabelle/HOL. Integration with ProofGeneral is provided.

Research Papers (and accompanying slides)

David von Oheimb, Georg Walter, and Volkmar Lotz: A Formal Security Model of the Infineon SLE 88 Smart Card Memory Management (the journal version of this paper contains a detailed description of the ISM semantics)
David von Oheimb and Volkmar Lotz: Generic Interacting State Machines and their instantiation with dynamic features
Thomas Kuhn and David von Oheimb: Interacting State Machines for Mobility
David von Oheimb: Interacting State Machines: a stateful approach to proving security
David von Oheimb and Volkmar Lotz: Formal Security Analysis with Interacting State Machines (recommended as an introduction to ISMs)
Sebastian Nanz: Integration of CASE Tools and Theorem Provers: A Framework for System Modeling and Verification with AutoFocus and Isabelle

User Manual including Specifications

Sebastian Nanz and David von Oheimb: Using the ISM Framework

Download

Theory sources

available upon request

URL: http://ddvo.net/ISM/index.html, Last modified: Sat Apr 23 23:46:44 CEST 2005