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)

User Manual including Specifications


URL:, Last modified: Thu Nov 19 19:07:34 CET 2009