AsmetaComp: A Tool for Runtime Contract Checking with I/O Abstract State Machines

Contract-based Design specifies components via assume–guarantee contracts, enabling modular development and verification. In state-based system modeling, it helps manage complexity through decomposition into analyzable sub-models coordinated by I/O events. However, its adoption is hindered by the lack of integrated languages and tools for the specification and verification of component contracts. This paper presents AsmetaComp, a tool that supports Contract-based Design for systems specified using I/O Abstract State Machines (ASMs), a state-based formalism for modeling and analyzing discrete-event systems. Originally developed for compositional simulation of interacting I/O ASM models, AsmetaComp has been extended to support Contract-based Design by integrating assume–guarantee contracts with executable I/O ASM models and enabling automated runtime contract checking during compositional execution. A healthcare case study is used to illustrate the tool and evaluate its effectiveness in supporting modular reasoning and dynamic contract checking in safety-critical, state-based systems.