Compositional Simulation of Abstract State Machines for Safety Critical Systems

Model-based simulation is nowadays an accepted practice for reliable prototyping of system behavior. To keep requirements complexity under control, system components are specified by separate models, validated and verified in isolation from the rest, but models have to be subsequently integrated and validated as a whole. For this reason, engines for orchestrated simulation of separate models are extremely useful. In this paper, we present a compositional simulation technique for managing the co-execution of Abstract State Machines (ASMs) communicating through I/O events. The proposed method allows the cosimulation of ASM models of separate subsystems of a Discrete Event System in a straight-through processing manner according to a predefined orchestration schema. We also present our experience in applying and validating the proposed technique in the context of the MVM (Mechanical Ventilator Milano) system, a mechanical lung ventilator that has been designed, successfully certified, and deployed during the COVID-19 pandemic.