TY - GEN
T1 - How to Efficiently Build a Front-End Tool for UPPAAL: 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/1
Y1 - 2017/10/1
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 Article in proceeding
SN - 978-3-319-69482-5
T3 - Lecture Notes in Computer Science
SP - 319
EP - 336
BT - Dependable Software Engineering. Theories, Tools, and Applications
A2 - Guldstrand Larsen, Kim
A2 - Sokolsky, Oleg
A2 - Wang, Ji
PB - Springer
CY - Cham
ER -