The McScM Framework
Research Publications
04/18/2012
The McScM Framework¶
Heußner, A.; Gall, T. L. & Sutre, G. McScM: A General Framework for the Verification of Communicating Machines Proc. of TACAS'12, Springer, 2012, 7214, 478-484
abstract¶
We present McScM, a platform for implementing and comparing verification algorithms for the class of finite-state processes exchanging messages over reliable, unbounded FIFO channels. McScM provides tools for the safety verification and controller synthesis of these infinite-state models. Our verification tool implements several model-checking techniques: CEGAR with different abstraction-refinement methods, abstract interpretation, abstract regular model checking, and lazy abstraction. Seen as a general framework for the class of transition systems with finite control/infinite data, McScM delivers the basic infrastructure for implementing verification algorithms, and privileges to conveniently implement new ideas on a high level of abstraction. It also allows us to compare and benchmark different algorithmic approaches with the same backend.
bibtex¶
@inproceedings{DBLP:conf/tacas/HeussnerGS12,
author = {Alexander Heu{\ss}ner and
Tristan Le Gall and
Gr{\'e}goire Sutre},
title = {McScM: A General Framework for the Verification of Communicating
Machines},
booktitle = {TACAS},
year = {2012},
pages = {478-484},
ee = {http://dx.doi.org/10.1007/978-3-642-28756-5_34},
crossref = {DBLP:conf/tacas/2012},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tacas/2012,
editor = {Cormac Flanagan and
Barbara K{\"o}nig},
title = {Tools and Algorithms for the Construction and Analysis of
Systems - 18th International Conference, TACAS 2012, Held
as Part of the European Joint Conferences on Theory and
Practice of Software, ETAPS 2012, Tallinn, Estonia, March
24 - April 1, 2012. Proceedings},
booktitle = {TACAS},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7214},
year = {2012},
isbn = {978-3-642-28755-8},
ee = {http://dx.doi.org/10.1007/978-3-642-28756-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}