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} }