COMPASS Modelling Language. The semantic model we use for VDM-RT is timed reactive designs, a form a specifica- tion construct that allows the specification of reactive behaviour with discrete timing constraints. This UTP theory is used to give a semantics to the COMPASS Modelling Language [29, 11] (CML), which is a combination of VDM-SL and the process algebra CSP. We give VDM-RT a UTP semantics by using CML, whose constructs are directly defined using the UTP. CML describes the behaviour of a system in terms of a collection of processes that commu- nicate with each other over shared synchronous channels. These channels can optionally carry data, and are the only way that processes can communicate. Each process addition- ally has a state structure which can be described using the data structures of VDM-SL, such as numerics, sets, sequences, records, and maps. This state is encapsulated, such that only constructs within the process’ scope can query the state variable. A CML process is described using a sequence of paragraphs that we summarise below: • the types paragraph, which describes the data structures the process uses; • the values paragraph, which describes static defined values of the process; • the state paragraph, which defines a collection of typed state variables; • the operations paragraph, which defines a collection of (non-reactive) operations that act on the state variables. They can be specified implicitly using pre- and postconditions; • the actions paragraph, which defines a collection of reactive actions that can both manipulate the state and interact with the environment using channels; • • the main action, P, which describes the top-level behaviour of a process using a composition of internal actions and operations.
