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


Theory sources

available upon request
URL:, Last modified: Sat Apr 23 23:46:44 CEST 2005