Correctness of an ATL Model Transformation from SysML State Machine Diagrams to Promela

被引：3

作者：

Caltais, Georgiana ^{[1
]}

Leue, Stefan ^{[1
]}

Singh, Hargurbir ^{[1
]}

机构：

[1] Univ Konstanz, Constance, Germany

来源：

PROCEEDINGS OF THE 8TH INTERNATIONAL CONFERENCE ON MODEL-DRIVEN ENGINEERING AND SOFTWARE DEVELOPMENT (MODELSWARD) | 2020年

关键词：

Model Transformation; ATL; SysML; Promela; Correctness; Observational Equivalence;

D O I：

10.5220/0008968303600372

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

In this paper we discuss the correctness of an ATL-based model transformation from the systems engineering modelling language SysML into Promela, the input language of the SPIN model checker. More precisely, we reduce showing the correctness of the transformation to showing a notion of what we refer to as observational equivalence of the SysML and the generated Promela models, respectively. This paves the way to a proof technique that could be further exploited in order to argue the correctness of model transformations from SysML to various model checkers, based on the observable actions generated by the systems under analysis.

引用

页码：360 / 372

页数：13

共 23 条

[1] Amrani M, 2015, J OBJECT TECHNOL, V14, DOI 10.5381/jot.2015.14.1.a3
[2] Anastasakis K., 2007, Model Driven Engineering, Verification, and Validation: Integrating Verification and Validation in MDE (MODEVVA07), P47
[3] Bengtsson J., 1996, Hybrid Systems III. Verification and Control, P232, DOI 10.1007/BFb0020949
[4] Buttner F., 2012, V7635
[5] Cimatti A., 2002, Computer Aided Verification. 14th International Conference, CAV 2002. Proceedings (Lecture Notes in Computer Science Vol.2404), P359
[6] Clavel M, 2003, LECT NOTES COMPUT SC, V2706, P76
[7] Dyck J., 2015, P 4 WORKSH AN MOD TR P 4 WORKSH AN MOD TR
[8] Engels G., 2008, LECT NOTES COMPUTER, V5095
[9] STATECHARTS - A VISUAL FORMALISM FOR COMPLEX-SYSTEMS
HAREL, D
[J]. SCIENCE OF COMPUTER PROGRAMMING, 1987, 8 (03) : 231 - &
[10] Holzmann G. J., 2004, The SPIN model checker: primer and reference manual, V1003

← 1 2 3 →