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

Fatima Shokri-Manninen, Leonidas Tsiopoulos, Jüri Vain, Marina Waldén
Digital Printed Abstract View Cite
Type
Conference paper
Publication
7th International Conference on Rigorous State Based Methods (ABZ'20)

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 verification 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 verification 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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{Shokri-Manninen20,
  author       = {Fatima Shokri{-}Manninen and
                  Leonidas Tsiopoulos and
                  J{\"{u}}ri Vain and
                  Marina Wald{\'{e}}n},
  editor       = {Alexander Raschke and
                  Dominique M{\'{e}}ry and
                  Frank Houdek},
  title        = {Integration of iUML-B and {UPPAAL} Timed Automata for Development
                  of Real-Time Systems with Concurrent Processes},
  booktitle    = {Rigorous State-Based Methods - 7th International Conference, {ABZ}
                  2020, Ulm, Germany, May 27-29, 2020, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12071},
  pages        = {186--202},
  publisher    = {Springer},
  year         = {2020},
  url          = {https://doi.org/10.1007/978-3-030-48077-6\_13},
  doi          = {10.1007/978-3-030-48077-6\_13},
  timestamp    = {Fri, 09 Apr 2021 18:50:59 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/Shokri-Manninen20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'20

Related