History

about the tool

McScM (Model Checker for Systems of Communicating fifo Machines) is a small framework for implementing model checking algorithms in the context of infinite state systems of the form "finite control plus infinite data". The main constituent is the verify tool for the safety verification of systems of communicating fifo machines (CFM). The goal of verify is the model checking of network protocols (given as CFM) with respect to a given set of undesired behaviours or "bad" states. The main difference to other tools for communicating automata is the modeling of asynchronous, reliable fifo channels which is indispensable for checking protocols that presuppose a reliable connection between the peers (for example as supplied by TCP or MPI). Further, the verify tool allows to choose among distinct verification algorithms which are itself highly parametrizable. This leads to a generic approach that can easily be adapted to a variety of concrete safety verification problems. In addition, McScM includes a tool for supervisory control that helps to fix unsafe protocols.

how to get it

Please refer to Download for instructions.

documentation and manual pages

We provide an online version of the manual pages of the tools included in McScM :
  • verify - safety verification of communicating machines
  • control - supervisory control for CFM
  • scm - CFM input language used by the previous two tools
We provide a description of McScM's OCaml module interfaces (separated into two packages):
  • Svar - safety verification by abstraction refinement
  • Util - utility functions

references

McScM is the outcome of our research on the application of counterexample-guided abstraction refinement methods to the model of communicating fifo machines.

A general introduction to McScM can be found in
  • Alexander Heußner, Tristan Le Gall, Grégoire Sutre: "McScM: A General Framework for the Verification of Communicating Machines", in Cormac Flanagan and Barbara König (ed.): Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 7214, pp. 478-484, Springer 2012 (local copy, slides)
More about the theoretical underpinning can be found in
  • Alexander Heußner, Tristan Le Gall, Grégoire Sutre: "Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems", in Corina Păsăreanu (ed.): Proceedings of the 16th Int. Workshop on Model Checking of Software (SPIN 2009), Grenoble, June 2009, LNCS 5578, pp. 107–124, Springer 2009 (local copy)
or even more detailled and with more background information in

or take a look at the slides.

The theoretical underpinning of the control tool (included since McScM 1.1) can be found in
  • Gabriel Kalyon, Tristan Le Gall, Hervé Marchand, Thierry Massart: "Global State Estimates for Distributed Systems", in Proceedings of the 31th IFIP International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'11), 2011 (local copy)
  • Gabriel Kalyon, Tristan Le Gall, Hervé Marchand, Thierry Massart, "Synthesis of Communicating Controllers for Distributed Systems", in Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (IEEE CDC-ECC'11), 2011.
First steps into the verification of systems that can exchange messages over an infinite message alphabet (e.g., exchange their local counters) can be found in
  • Alexander Heussner, Tristan Le Gall, and Grégoire Sutre: "Safety Verification of Communicating One-Counter Machines", in Proceedings. IARCS Ann. Conf. Found. of Software Technology and Theor. Comp. Sci. (FSTTCS'12), vol. 18 of LIPIcs, pages 224-235, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. (direct link to online version http://drops.dagstuhl.de/opus/volltexte/2012/3861/pdf/22.pdf)

acknowledgements

We gratefully thank Bertrand Jeannet and Tristan Le Gall for their inspiring work on abstract interpretation for Systems of Communicating fifo Machines [AMAST06] [SAS07]. Our tool uses (slightly adapted versions) of their OCaml packages latticeAutomata for representing recognizable languages and their extrapolation, as well as scm for parsing and calculating communicating machines; both can be found at http://gforge.inria.fr/projects/bjeannet/ . Also thanks to Ivan Beschastnikh for feedback and ideas for making the McScM tools better accessible to new users.

contact

mailto:(λ x · x @uni-bamberg.de)(alexander.heussner)
mailto:(λ x · x @labri.fr)(gregoire.sutre)
mailto:(λ x · x @cea.fr)(tristan.le-gall)

Please feel free to contact us in case you want further information, want to report a bug, or due to any other reason except filling our mailboxes with spam.