Automatic Generation of Functional Mock-Up Units from Formal Specifications

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer review

DOI

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.
OriginalsprogEngelsk
TitelSoftware Engineering and Formal Methods
RedaktørerJavier Camara, Martin Steffen
Antal sider7
UdgivelsesstedCham
ForlagSpringer
Udgivelsesår2020
Sider27-33
ISBN (trykt)978-3-030-57505-2
ISBN (Elektronisk)978-3-030-57506-9
DOI
StatusUdgivet - 2020
BegivenhedInternational Conference on Software Engineering and Formal Methods
- Oslo, Norge
Varighed: 16 sep. 201920 sep. 2019

Konference

KonferenceInternational Conference on Software Engineering and Formal Methods
LandNorge
ByOslo
Periode16/09/201920/09/2019
SerietitelLecture Notes in Computer Science
Vol/bind12226
ISSN0302-9743

Se relationer på Aarhus Universitet Citationsformater

ID: 196569639