How to Efficiently Build a Front-End Tool for UPPAAL: A Model-Driven Approach

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2 Citations

Abstract

We propose a model-driven engineering approach that facilitates the production of tool chains that use the popular model checker Uppaal as a back-end analysis tool. In this approach, we introduce a metamodel for Uppaal’s input model, containing both timed-automata concepts and syntax-related elements for C-like expressions. We also introduce a metamodel for Uppaal’s query language to specify temporal properties; as well as a metamodel for traces to interpret Uppaal’s counterexamples and witnesses. The approach provides a systematic way to build software bridging tools (i.e., tools that translate from a domain-specific language to Uppaal’s input language) such that these tools become easier to debug, extend, reuse and maintain. We demonstrate our approach on five different domains: cyber-physical systems, hardware-software co-design, cyber-security, reliability engineering and software timing analysis.
LanguageEnglish
Title of host publicationDependable Software Engineering. Theories, Tools, and Applications
Subtitle of host publicationThird International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings
EditorsKim Larsen, Oleg Sokolsky, Ji Wang
PublisherSpringer
Pages319-336
ISBN (Electronic)978-3-319-69483-2
ISBN (Print)978-3-319-69482-5
DOIs
StatePublished - Oct 2017
Event3rd International Symposium on Dependable Software Engineering, SETTA 2017 - Changsha, China
Duration: 23 Oct 201725 Oct 2017
Conference number: 3
http://lcs.ios.ac.cn/setta2017/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10606
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameLecture Notes in Programming and Software Engineering
PublisherSpringer

Conference

Conference3rd International Symposium on Dependable Software Engineering, SETTA 2017
Abbreviated titleSETTA
CountryChina
CityChangsha
Period23/10/1725/10/17
Internet address

Fingerprint

Query languages
Computer hardware
Cyber Physical System

Cite this

Schivo, S., Yildiz, B. M., Ruijters, E. J. J., Gerking, C., Kumar, R., Dziwok, S., ... Stoelinga, M. I. A. (2017). How to Efficiently Build a Front-End Tool for UPPAAL: A Model-Driven Approach. In K. Larsen, O. Sokolsky, & J. Wang (Eds.), Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings (pp. 319-336). (Lecture Notes in Computer Science; Vol. 10606), (Lecture Notes in Programming and Software Engineering). Springer. DOI: 10.1007/978-3-319-69483-2_19
Schivo, Stefano ; Yildiz, Bugra Mehmet ; Ruijters, Enno Jozef Johannes ; Gerking, Christopher ; Kumar, Rajesh ; Dziwok, Stefan ; Rensink, Arend ; Stoelinga, Mariëlle Ida Antoinette. / How to Efficiently Build a Front-End Tool for UPPAAL : A Model-Driven Approach. Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings. editor / Kim Larsen ; Oleg Sokolsky ; Ji Wang. Springer, 2017. pp. 319-336 (Lecture Notes in Computer Science). (Lecture Notes in Programming and Software Engineering).
@inproceedings{0a7f1ca2ca554ddbb8be834b00258cd0,
title = "How to Efficiently Build a Front-End Tool for UPPAAL: A Model-Driven Approach",
abstract = "We propose a model-driven engineering approach that facilitates the production of tool chains that use the popular model checker Uppaal as a back-end analysis tool. In this approach, we introduce a metamodel for Uppaal’s input model, containing both timed-automata concepts and syntax-related elements for C-like expressions. We also introduce a metamodel for Uppaal’s query language to specify temporal properties; as well as a metamodel for traces to interpret Uppaal’s counterexamples and witnesses. The approach provides a systematic way to build software bridging tools (i.e., tools that translate from a domain-specific language to Uppaal’s input language) such that these tools become easier to debug, extend, reuse and maintain. We demonstrate our approach on five different domains: cyber-physical systems, hardware-software co-design, cyber-security, reliability engineering and software timing analysis.",
author = "Stefano Schivo and Yildiz, {Bugra Mehmet} and Ruijters, {Enno Jozef Johannes} and Christopher Gerking and Rajesh Kumar and Stefan Dziwok and Arend Rensink and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
year = "2017",
month = "10",
doi = "10.1007/978-3-319-69483-2_19",
language = "English",
isbn = "978-3-319-69482-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "319--336",
editor = "Kim Larsen and Oleg Sokolsky and Ji Wang",
booktitle = "Dependable Software Engineering. Theories, Tools, and Applications",

}

Schivo, S, Yildiz, BM, Ruijters, EJJ, Gerking, C, Kumar, R, Dziwok, S, Rensink, A & Stoelinga, MIA 2017, How to Efficiently Build a Front-End Tool for UPPAAL: A Model-Driven Approach. in K Larsen, O Sokolsky & J Wang (eds), Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10606, Lecture Notes in Programming and Software Engineering, Springer, pp. 319-336, 3rd International Symposium on Dependable Software Engineering, SETTA 2017, Changsha, China, 23/10/17. DOI: 10.1007/978-3-319-69483-2_19

How to Efficiently Build a Front-End Tool for UPPAAL : A Model-Driven Approach. / Schivo, Stefano ; Yildiz, Bugra Mehmet; Ruijters, Enno Jozef Johannes; Gerking, Christopher; Kumar, Rajesh ; Dziwok, Stefan; Rensink, Arend ; Stoelinga, Mariëlle Ida Antoinette.

Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings. ed. / Kim Larsen; Oleg Sokolsky; Ji Wang. Springer, 2017. p. 319-336 (Lecture Notes in Computer Science; Vol. 10606), (Lecture Notes in Programming and Software Engineering).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - How to Efficiently Build a Front-End Tool for UPPAAL

T2 - A Model-Driven Approach

AU - Schivo,Stefano

AU - Yildiz,Bugra Mehmet

AU - Ruijters,Enno Jozef Johannes

AU - Gerking,Christopher

AU - Kumar,Rajesh

AU - Dziwok,Stefan

AU - Rensink,Arend

AU - Stoelinga,Mariëlle Ida Antoinette

PY - 2017/10

Y1 - 2017/10

N2 - We propose a model-driven engineering approach that facilitates the production of tool chains that use the popular model checker Uppaal as a back-end analysis tool. In this approach, we introduce a metamodel for Uppaal’s input model, containing both timed-automata concepts and syntax-related elements for C-like expressions. We also introduce a metamodel for Uppaal’s query language to specify temporal properties; as well as a metamodel for traces to interpret Uppaal’s counterexamples and witnesses. The approach provides a systematic way to build software bridging tools (i.e., tools that translate from a domain-specific language to Uppaal’s input language) such that these tools become easier to debug, extend, reuse and maintain. We demonstrate our approach on five different domains: cyber-physical systems, hardware-software co-design, cyber-security, reliability engineering and software timing analysis.

AB - We propose a model-driven engineering approach that facilitates the production of tool chains that use the popular model checker Uppaal as a back-end analysis tool. In this approach, we introduce a metamodel for Uppaal’s input model, containing both timed-automata concepts and syntax-related elements for C-like expressions. We also introduce a metamodel for Uppaal’s query language to specify temporal properties; as well as a metamodel for traces to interpret Uppaal’s counterexamples and witnesses. The approach provides a systematic way to build software bridging tools (i.e., tools that translate from a domain-specific language to Uppaal’s input language) such that these tools become easier to debug, extend, reuse and maintain. We demonstrate our approach on five different domains: cyber-physical systems, hardware-software co-design, cyber-security, reliability engineering and software timing analysis.

U2 - 10.1007/978-3-319-69483-2_19

DO - 10.1007/978-3-319-69483-2_19

M3 - Conference contribution

SN - 978-3-319-69482-5

T3 - Lecture Notes in Computer Science

SP - 319

EP - 336

BT - Dependable Software Engineering. Theories, Tools, and Applications

PB - Springer

ER -

Schivo S, Yildiz BM, Ruijters EJJ, Gerking C, Kumar R, Dziwok S et al. How to Efficiently Build a Front-End Tool for UPPAAL: A Model-Driven Approach. In Larsen K, Sokolsky O, Wang J, editors, Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings. Springer. 2017. p. 319-336. (Lecture Notes in Computer Science). (Lecture Notes in Programming and Software Engineering). Available from, DOI: 10.1007/978-3-319-69483-2_19