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 Walden

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussaKonferenssiartikkeliTieteellinenvertaisarvioitu

3 Sitaatiot (Scopus)
46 Lataukset (Pure)

Abstrakti

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.
AlkuperäiskieliEnglanti
OtsikkoRigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings
ToimittajatAlexander Raschke, Dominique Méry, Frank Houdek
KustantajaSpringer
Sivut186-202
ISBN (elektroninen)978-3-030-48077-6
ISBN (painettu)978-3-030-48076-9
TilaJulkaistu - 2020
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational Conference on Rigorous State-Based Methods - ABZ 2020 – 7th International Conference on Rigorous State Based Methods
Kesto: 27 toukok. 202029 toukok. 2020

Julkaisusarja

NimiLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vuosikerta12071 LNCS
ISSN (painettu)0302-9743
ISSN (elektroninen)1611-3349

Konferenssi

KonferenssiInternational Conference on Rigorous State-Based Methods
Ajanjakso27/05/2029/05/20

Keywords

  • Formal verification
  • Model checking

Sormenjälki

Sukella tutkimusaiheisiin 'Integration of iUML-B and UPPAAL Timed Automata for Development of Real-Time Systems with Concurrent Processes'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Viittausmuodot