A Compositional Simulation Framework for Abstract State Machine Models of Discrete Event Systems

Modeling complex system requirements often requires specifying system components in separate models, which can be validated and verified in isolation from each other, and then integrating all components' behavior in order to validate the operation of the whole system. If models are executable, as for state-based formal specifications, engines to orchestrate the simulation of separate component operational models are extremely useful. This paper presents an approach for the co-simulation, according to predefined orchestration schemas, of state-based models of separate components of a Discrete Event System. More precisely, we exploit the Abstract State Machine (ASM) formal method as state-based formalism, and we (i) define a set of operators to compose ASMs that communicate with each other through I/O events, and (ii) present an engine to execute the compositional simulation of the ASMs as a whole assembly. As proof of concepts, we use a set of model examples of Discrete Event Systems of increasing complexity to show the application of our approach and to evaluate its effectiveness in co-simulating models of real systems.