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
available upon request
Last modified: Sat Apr 23 23:46:44 CEST 2005