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

Georgiana Caltais | Zendy; Stefan Leue | Zendy; Hargurbir Singh | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

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

Author(s) -

Georgiana Caltais,

Stefan Leue,

Hargurbir Singh

Publication year - 2020

Publication title -

kops (university of konstanz)

Language(s) - English

Resource type - Conference proceedings

DOI - 10.5220/0008968303600372

Subject(s) - promela , correctness , computer science , systems modeling language , model checking , programming language , model transformation , transformation (genetics) , state (computer science) , abstract state machines , finite state machine , unified modeling language , artificial intelligence , software , consistency (knowledge bases) , biochemistry , chemistry , gene

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research