The operational behaviour of a reactive system is commonly specified or modelled as concurrent state machines, where each machine models the possible states or modes of a software component and its interactions with the environment. However, state machines can quickly become verbose when execution constraints between concurrent states need to be modelled. Alternatively, constraints could be modelled declaratively as special edges between states. Such a heterogeneous modelling approach is employed by Virtual Satellite (VirSat), a model-based systems engineering tool from the German Aerospace Center (DLR). The challenge has been to develop a heterogeneous modelling framework that supports an operational and declarative syntax, defines a unified semantics suitable for formal reasoning, and supports the independent and incremental development of software components.
We address this challenge with our Component State Machine (CSM) formalism as a means to operationalise VirSat: the operational syntax of VirSat is preserved in CSM, the declarative VirSat constraints are transformed into CSM atomic propositions and parallel conditions, the CSM parallel operator incrementally composes CSMs and resolves the parallel conditions, and design errors are analysed as inconsistent transitions. CSM permits new constraints to be defined without needing to modify the core VirSat semantics. We also propose an intuitive, practical, and mathematically rigorous notion of refinement that aims to encourage a more systematic development of spacecraft software. Lastly, we offer a modular implementation of CSMs as hierarchically scheduled Executable State Machines (ESMs) that remains open to further composition and refinement.