Zusammenfassung:
The subject of this thesis is the introduction of the concept of “contracts” to modal transition systems. It aims to provide intuitive notions of contract satisfaction by introducing a “relativized refinement” relation, together with the concept of a “normal form” where satisfaction equals normal strong modal refinement. Additionally, operations on modal transition systems are extended to contracts. As a practical aspect, it extends the MIO Workbench, a formal verification tool for modal input/output automata, to accommodate the design of and operations on contracts.
Download:
N/A