In this paper we present an automated translation from the systems engineering modeling language SysML into the input languages of the NuSMV, Prism and Spin model checkers. A special focus of this work is the semantics of the communication mechanisms used in a syntactic fragment of SysML, in particular synchronous and asynchronous, broadcast and buffered communication. In order to achieve generality of our approach, which supports establishing the consistency of the translation as well as enabling easy adaption between different source and target languages, we use a model based transformation approach. In particular, we use the ATLAS Transformation Language (ATL) framework that is nicely integrated in the Eclipse Modeling Framework (EMF) and in the Meta-Object Facility. We illustrate the application of this model transformation approach using an airbag system as a case study.
展开▼
