@inproceedings{DBLP:conf/models/KanavA17, author = {Kanav, Sudeep and Aravantinos, Vincent}, title = {Modular Transformation from {AF3} to nuXmv}, booktitle = {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}, pages = {300--306}, year = {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.}, keywords = {AutoFOCUS3, formal verification, model-based systems engineering, MbSE}, url = {http://ceur-ws.org/Vol-2019/modevva_1.pdf}, crossref = {DBLP:conf/models/2017s}, }