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.
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
Last modified: Thu Nov 19 19:07:34 CET 2009