ICE-TCS seminar: Georgiana Caltais
Correctness of an ATL Model Transformation from SysML to Spin
ICE-TCS seminar #332
Date and time: Tuesday, 23 April 2019, 12:10-13:00
Location: Room M1.11
Speaker: Georgiana Caltais, University of Konstanz, Germany WWW: https://dl.dropboxusercontent.com/u/1356725/caltais/index.html
Title: Correctness of an ATL Model Transformation from SysML to Spin
Abstract: In this talk I will present an approach to showing the correctness of an ATL-based model transformation from the systems engineering modelling language SysML into the input language of the Spin model checker. The approach consists of showing a notion of so-called observational equivalence of the SysML and the generated Spin 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.
This is a joint work with Stefan Leue and Hargurbir Singh at the University of Konstanz, Germany.
