Modular Transformation from AF3 to nuXmv

Sudeep Kanav and Vincent Aravantinos

Proceedings of MODELS 2017 Satellite Event: Workshops (ModComp, ME, EXE, COMMitMDE, MRT, MULTI, GEMOC, MoDeVVa, MDETools, FlexMDE, MDEbug), Posters, Doctoral Symposium, Educator Symposium, ACM Student Research Competition, and Tools and Demonstrations, pp. 300–306

2017

abstract

AutoFOCUS3 (AF3) supports formal verification of its models using the nuXmv model checker. This requires a model transformation from AF3 to nuXmv models. In this paper we present this behavior transformation. It is a two way transformation between a high-level and a low-level model involving intricate cases typical of behavior transformations whose solutions can therefore be beneficial to the community.

subject terms: AutoFOCUS3, formal verification, model-based systems engineering, MbSE

url: http://ceur-ws.org/Vol-2019/modevva_1.pdf

URL BibTeX Back