ICE-TCS seminar: Georgiana Caltais

Correctness of an ATL Model Transformation from SysML to Spin

  • 23.4.2019, 12:10 - 13:00

ICE-TCS-logo-200px

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.