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

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

Forskningsoutput: Kapitel i bok/konferenshandling › Publicerad konferensartikel › Vetenskaplig › Peer review

5 Citeringar (Scopus)

100 Nedladdningar (Pure)

Sammanfattning

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.

Originalspråk	Engelska
Titel på värdpublikation	Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings
Redaktörer	Alexander Raschke, Dominique Méry, Frank Houdek
Förlag	Springer
Sidor	186-202
ISBN (elektroniskt)	978-3-030-48077-6
ISBN (tryckt)	978-3-030-48076-9
Status	Publicerad - 2020
MoE-publikationstyp	A4 Artikel i en konferenspublikation
Evenemang	International Conference on Rigorous State-Based Methods - ABZ 2020 – 7th International Conference on Rigorous State Based Methods Varaktighet: 27 maj 2020 → 29 maj 2020

Publikationsserier

Namn	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volym	12071 LNCS
ISSN (tryckt)	0302-9743
ISSN (elektroniskt)	1611-3349

Konferens

Konferens	International Conference on Rigorous State-Based Methods
Period	27/05/20 → 29/05/20

Finansiering

Acknowledgments. This work has received funding from the Electronic Component Systems for European Leadership Joint Undertaking under grant agreement No 737494. This Joint Undertaking receives support from the European Union’s Horizon 2020 research and innovation programme and Sweden, France, Spain, Italy, Finland, the Czech Republic. This was also supported by the ERDF funded centre of excellence project EXCITE (2014-2020.4.01.15-0018) and the Estonian Ministry of Education and Research institutional research grant no. IUT33-13.

Nyckelord

Formal verification
Model checking

Åtkomst av dokument

ABZ2020_Camera_ready.pdfAccepterat manuskript från författare, 1,78 MBLicens: CC BY

Citera det här

Shokri-Manninen, F., Tsiopoulos, L., Vain, J., & Walden, M. (2020). Integration of iUML-B and UPPAAL Timed Automata for Development of Real-Time Systems with Concurrent Processes. I A. Raschke, D. Méry, & F. Houdek (Red.), Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings (s. 186-202). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12071 LNCS). Springer. http://urn.fi/URN:NBN:fi-fe2020102788603

Shokri-Manninen, Fatima ; Tsiopoulos, Leonidas ; Vain, Jüri et al. / Integration of iUML-B and UPPAAL Timed Automata for Development of Real-Time Systems with Concurrent Processes. Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings. redaktör / Alexander Raschke ; Dominique Méry ; Frank Houdek. Springer, 2020. s. 186-202 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{b0b0914273bc4916b84e5eb932da5d26,

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

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.",

keywords = "Formal verification, Model checking, Formal verification, Model checking, Formal verification, Model checking",

author = "Fatima Shokri-Manninen and Leonidas Tsiopoulos and J{\"u}ri Vain and Marina Walden",

year = "2020",

language = "English",

isbn = "978-3-030-48076-9",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "186--202",

editor = "Alexander Raschke and Dominique M{\'e}ry and Frank Houdek",

booktitle = "Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings",

note = "International Conference on Rigorous State-Based Methods ; Conference date: 27-05-2020 Through 29-05-2020",

}

Shokri-Manninen, F, Tsiopoulos, L, Vain, J & Walden, M 2020, Integration of iUML-B and UPPAAL Timed Automata for Development of Real-Time Systems with Concurrent Processes. i A Raschke, D Méry & F Houdek (red), Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12071 LNCS, Springer, s. 186-202, International Conference on Rigorous State-Based Methods, 27/05/20. <http://urn.fi/URN:NBN:fi-fe2020102788603>

Integration of iUML-B and UPPAAL Timed Automata for Development of Real-Time Systems with Concurrent Processes. / Shokri-Manninen, Fatima; Tsiopoulos, Leonidas; Vain, Jüri et al.
Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings. red. / Alexander Raschke; Dominique Méry; Frank Houdek. Springer, 2020. s. 186-202 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12071 LNCS).

Forskningsoutput: Kapitel i bok/konferenshandling › Publicerad konferensartikel › Vetenskaplig › Peer review

TY - GEN

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

AU - Shokri-Manninen, Fatima

AU - Tsiopoulos, Leonidas

AU - Vain, Jüri

AU - Walden, Marina

PY - 2020

Y1 - 2020

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

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

KW - Formal verification

KW - Model checking

KW - Formal verification

KW - Model checking

KW - Formal verification

KW - Model checking

M3 - Published conference proceeding

SN - 978-3-030-48076-9

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 186

EP - 202

BT - Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings

A2 - Raschke, Alexander

A2 - Méry, Dominique

A2 - Houdek, Frank

PB - Springer

T2 - International Conference on Rigorous State-Based Methods

Y2 - 27 May 2020 through 29 May 2020

ER -

Shokri-Manninen F, Tsiopoulos L, Vain J, Walden M. Integration of iUML-B and UPPAAL Timed Automata for Development of Real-Time Systems with Concurrent Processes. I Raschke A, Méry D, Houdek F, redaktörer, Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings. Springer. 2020. s. 186-202. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

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

Sammanfattning

Publikationsserier

Konferens

Finansiering

Nyckelord

Åtkomst av dokument

Fingeravtryck

Citera det här