Automatic Generation of Functional Mock-Up Units from Formal Specifications

This paper reports on the approach used to augment a transition system tool with automatic Functional Mock-up Units (FMU) generation. To verify the FMU properties, the same transition system can be translated into a formal language. Among intrinsic system properties, transition systems are associated with the following two: the disjointedness and the coverage, which assert that the controller is deterministic and defined for every possible input. This paper shows how both properties are enforced when proving the type checking conditions derived by the PVS theorem prover.