Moded and Continuous Abstract State Machines

In view of the increasing importance of cyber-physical systems, and of their correct design, the Abstract State Machine (ASM) framework is extended to include continuously varying quantities as well as the conventional discretely changing ones. This opens the door to the more faithful modelling of many scenarios where digital systems have to interact with the continuously varying physical world. Transitions in the extended framework are thus either moded (catering for discontinuously changing quantities), or pliant (catering for smoothly changing quantities). An operational semantics is provided, first for monolithic systems, and this is then extended to give a semantics for systems consisting of several distinct subsystems. This allows each subsystem to undergo its own subsystem-specific mode and pliant transitions. Refinement is elaborated in the extended context for both monolithic and composed systems. The formalism is illustrated using an example of a bouncing tennis ball.