Architecture Instantiation. Before we consider the relational and Circus model of FMUs, we instantiate the FMI architecture by assigning concrete values to the abstract constants in Fig. 9 (p. 33). As previously noted, this instantiation is also discussed in INTO-CPS Deliverable D2.3a, where it is serves to establish well-formedness of an architecture. In this deliverable, it is a key ingredient for defining the concrete behaviour of a master algorithm. We hence summarise it, focusing on aspects relevant to the work here. To instantiate the abstract type FMI2COMP, we make use of an Isabelle/HOL axiomatization that introduces concrete symbolic constants for each of the FMUs. In this case, we call them train1, train2, merger and interlocking. Fig. 17 includes the corresponding mechanisation fragment. We note that Isabelle axiomatizations can potentially cause logical inconsis- tencies in HOL theories. Here, however, the particular shape of the assump- tions, being that of an enumerated type, guarantees consistency. The INTO-SysML diagram (Fig. 14) is encoded by providing definitions for the seven constants: FMUs, parameters, initialValues, inputs, outputs, pdg and idd. We note that those definitions, unlike the previous one, are xxxxxx- vative — no user-level axioms are hence required to formulate them. As mentioned earlier on, FMUs is a sequence of all FMUs, hence we require its range to include all the values of the FMI2COMP type. Below we recapture its definition for the railways co-simulation system. Figure 18: Parameter definition of the railways instantiation. × × We recall that simulation parameters are of type FMI2COMP VAR VAL. Con- crete parameters of the railways co-simulation are the routes of the trains and their maximum speed. Fig. 18 illustrates parameter instantiation in Is- abelle. The function InjU is used to construct a value of type VAL from some arbitrary HOL value; it is part of our universal value model [30] and allows us to encode arbitrary HOL values as elements of a universal type VAL. Our syntax for constructing variables is $name:{type}. The types fmi2Integer and fmi2Real are synonyms for the HOL types int and real, encoding inte- gers and real numbers, respectively. Indeed, we introduce such synonyms for all permissible FMI port types as per the FMI standard 2.0 [1]. × Next, we consider the input and output ports of the control diagram in Fig. 14 on page 42. We recall that ports are modelled by pairs of type FMI2COMP VAR. An extract of the definition of in...
