Integration of iUML-B and UPPAAL Timed Automata for Development of Real-Time
Systems with Concurrent Processes

A4 Conference proceedings


Internal Authors/Editors


Publication Details

List of Authors: Fatima Shokri-Manninen, Leonidas Tsiopoulos, Jüri Vain, and Marina Waldén
Editors: Dominique Mery ,
Alexander Raschke
Place: Ulm, Germany
Publication year: 2020
Book title: Proceedings of ABZ 2020 - 7th International Conference on Rigorous State Based Methods


Abstract

Developing safety-critical systems requires to consider safety

and real-time requirements in addition to functional requirements. Event-

B is a formalism that is visualised by iUML-B and supports the development

of functional aspects having rich veri cation and validation tools.

However, it lacks well-established support for timing analysis. UPPAAL

Timed Automata (UTA), on the other hand, address timing aspects of

systems, and enable model checking reachability and timing properties.

By integrating iUML-B and UTA, we combine the best verifying and validating

practices from the two methods achieving a formal development

of systems.We present the mapping for translating iUML-B constructs to

UTA. The novel aspect is the use of a multi-process trigger-response pattern

to address the modelling and veri cation of reachability properties

of complex systems with concurrent processes. The approach is demonstrated

on an airport control system, where timing, fairness, as well as

liveness properties play a vital role in proving safety requirements.


Keywords

Formal verification, Model checking


Documents


Last updated on 2020-01-06 at 05:44