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

Files

heussner-a-2012-478-a.pdf - proceedings publication (280.6 kB) Alexander Heußner, 04/18/2012 02:03 pm

McScM_TACAS12_talk.pdf - slides of presentation (6.1 MB) Alexander Heußner, 04/18/2012 02:03 pm