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

Research output: Chapter in Book/Conference proceeding › Published conference proceeding › Scientific › peer-review

5 Citations (Scopus)

100 Downloads (Pure)

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.

Original language	English
Title of host publication	Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings
Editors	Alexander Raschke, Dominique Méry, Frank Houdek
Publisher	Springer
Pages	186-202
ISBN (Electronic)	978-3-030-48077-6
ISBN (Print)	978-3-030-48076-9
Publication status	Published - 2020
MoE publication type	A4 Article in a conference publication
Event	International Conference on Rigorous State-Based Methods - ABZ 2020 – 7th International Conference on Rigorous State Based Methods Duration: 27 May 2020 → 29 May 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12071 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

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

Funding

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.

Keywords

Formal verification
Model checking

Access to Document

ABZ2020_Camera_ready.pdfAccepted author manuscript, 1.78 MBLicence: CC BY

Cite this

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. In A. Raschke, D. Méry, & F. Houdek (Eds.), Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings (pp. 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. editor / Alexander Raschke ; Dominique Méry ; Frank Houdek. Springer, 2020. pp. 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. in A Raschke, D Méry & F Houdek (eds), 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, pp. 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. ed. / Alexander Raschke; Dominique Méry; Frank Houdek. Springer, 2020. p. 186-202 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12071 LNCS).

Research output: Chapter in Book/Conference proceeding › Published conference proceeding › Scientific › 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. In Raschke A, Méry D, Houdek F, editors, Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Proceedings. Springer. 2020. p. 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

Abstract

Publication series

Conference

Funding

Keywords

Access to Document

Fingerprint

Cite this