@inproceedings{horvath-openmbee-2020,
author = {Horv\'{a}th, Benedek and Graics, Bence and Hajdu, \'{A}kos and Micskei, Zolt\'{a}n and Moln\'{a}r, Vince and R\'{a}th, Istv\'{a}n and Andolfato, Luigi and Gomes, Ivan and Karban, Robert},
title = {Model Checking as a Service: Towards Pragmatic Hidden Formal Methods},
year = {2020},
isbn = {9781450381352},
publisher = {Association for Computing Machinery},
doi = {10.1145/3417990.3421407},
abstract = {Executable models can be used to support all engineering activities in Model-Based Systems Engineering. Testing and simulation of such models can provide early feedback about design choices. However, in today's complex systems, failures could arise due to subtle errors that are hard to find without checking all possible execution paths. Formal methods, and especially model checking can uncover such subtle errors, yet their usage in practice is limited due to the specialized expertise and high computing power required. Therefore we created an automated, cloud-based environment that can verify complex reachability properties on SysML State Machines using hidden model checkers. The approach and the prototype is illustrated using an example from the aerospace domain.},
booktitle = {Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings},
articleno = {37},
numpages = {5},
keywords = {MBSE, model checking, verification, SysML},
}