Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Domain-specific model checking for cyber-physical systems

 
: Gerking, C.; Schäfer, W.; Dziwok, S.; Heinzemann, C.

:
Fulltext (PDF; )

Famelis, Michalis:
12th Workshop on Model-Driven Engineering, Verification and Validation, MoDeVVa 2015. Proceedings. Online resource : Co-located with ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (MODELS 2015); Ottawa, Canada, September 29, 2015
Ottawa, 2015 (CEUR Workshop Proceedings 1514)
http://ceur-ws.org/Vol-1514/
pp.18-27
Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa) <12, 2015, Ottawa>
International Conference on Model Driven Engineering Languages and Systems (MODELS) <18, 2015, Ottawa>
English
Conference Paper, Electronic Publication
Fraunhofer IPT ()

Abstract
Cyber-physical systems (CPS) require model checking to guarantee the functional correctness of software models, providing counterexamples in case of violations. Domain-specific model checking (DSMC) allows to apply model checking to specific application domains. DSMC hides the complexity of using a model checker by translating from a domain-specific modeling language (DSML) to the model checker's input language, and by translating counterexamples back to the domain-specific level. Implementing DSMC is challenging for CPS due to the large differences between DSMLs and the input language of a model checker. In this paper, we present a successful application of DSMC to MECHATRONICUML, a DSML for the software design of CPS, using the model checker UPPAAL. As a key benefit, our approach is able to translate counterexamples back to the domain-specific level even in case of large differences between DSML and the model checker's input language. We show the correctness of our approach using a case study from the area of car-2-car communication.

: http://publica.fraunhofer.de/documents/N-418264.html