A Unified Formulation of Behavioral Semantics for SysML Models

Christoph Hilken, Jan Peleska, Robert Wille

In: Modelsward 3rd International Conference on Model-Driven Engineering and Software Development. International Conference on Model-Driven Engineering and Software Development (MODELSWARD-2015) 3rd February 9-11 Angers France 2015.


In order to cope with the complexity of today's system designs, higher levels of abstraction are considered. Modeling languages such as SysML provide adequate description means for an abstract specification of the structure and the behavior of a system to be implemented. Due to its sufficient degree of formality, SysML additionally allows for performing several automated test and verification tasks. For these tasks, however, a formal encoding of the behavioral model semantics is required; this is typically achieved by generating initial state conditions as well as the transition relation from the model. Since SysML provides a multitude of alternative or complementary notations, this poses a significant challenge to the development of corresponding tool support. In this paper, we therefore propose an alternative approach to the generation of transition relations: In a first step, a model-to-model transformation is applied which unifies the behavioral descriptions into one single notation, namely operations allocated in blocks and specified by pre- and post-conditions. Afterwards, only pre- and post-conditions as well as some auxiliary constraints for fixing semantic variation points need to be considered when generating the transition relation. The approach presented here has been evaluated in the development of industrial tools supporting bounded model checking and model-based test generation.


Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence