VDM-RT Interlocking FMU Sample Clauses

VDM-RT Interlocking FMU. For the encoding of the interlocking FMU, we first declare an alphabet that introduces the variables for the FMU inputs, outputs, state and time. We make use of the vector type to represent fixed vectors of booleans and switch configurations. The type switch is introduced to represent the possi- ble orientations of a railway switch. Railways switches can either be set to STRAIGHT or DIVERGING. Lastly, the variable time records simulation time; we use it to impose restrictions on admissible simulation step sizes. We note that the above is in direct correspondence with the VDM-RT model of the software controller of the FMU. The complete VDM-RT model of the controller is included in Appendix A. The four major sequential tasks discussed in Section 5.1.2 can now be directly translated into a sequential program within Isabelle/UTP that corresponds to the periodic behaviour of the controller in each execution cycle. For instance, Fig. 21 includes the encoding of the relay activation operations in Fig. 16 on page 45. Conditional if statements are encoded here using the infix syntax PabdQ of the UTP [20]. Here, b is the condition, and P and Q correspond to Figure 21: Encoding of the VDM-RT code fragment for setting relays. the then and else branch. We also note that CDV[i] and TC[i] are a custom syntax to access the elements of the vectors cdv and tc of the state. The other sequential fragments clear relays, set switches and set relays are encoded in a similar fashion. We point to the Isabelle technical report [29] for their definition. We, lastly, have a statement that determines the admissible increase of sim- ulation time, via the time variable. Here, this is modelled as an assignment that (deterministically) increases time by the period of the periodic thread of the cyclic executive for the interlocking program. This gives us the following complete relational FMU model of the interlocking: Above, δ is introduced as a constant for the thread period. This means that the simulation step size of the entire co-simulation is determined by the interlocking FMU, and corresponding to the execution period of the hardware controller of the interlocking. The process lifting discussed in the next section ensures that we respect admissible simulation step sizes, raising fmi2Discard signals when necessary. The CDV/TC Merger FMU is encoded in a similar manner. Its key func- tionality is to set the elements of the cdv and tc vectors according to the current track[1/2] and telec...