SARMC - Spotlight Abstraction Refinement Model Checker





Model reduction


SARMC addresses the formal verification of distributed systems comprising a dynamically changing and potentially unbounded number of processes. SARMC employs the spotlight principle to obtain a concise finitary abstraction of the system and devises an abstraction refinement strategy guided by the analysis of abstract counterexamples. The tool reads an XML description of a Dynamic Evolution System (DES) and an ASCII text-file specifying the requirement. A compiler from Dynamic Communication Systems (DCS) to DES is also integrated, including the computation of communication invariants for DCS. The VIS model checker is used as verification back-end.


T. Toben. Counterexample guided spotlight abstraction refinement. In Kenji Suzuki, Teruo Higashino, Keiichi Yasumoto, and Khaled El-Fakih, editors, Proceedings of the 28th International Federation for Information Processing (IFIP) WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), volume 5048 of Lecture Notes in Computer Science (LNCS), pages 21-36, 2008. Best Paper Award.

T. Toben. Non-Interference Properties for the Data-Type Reduction of Communicating Systems. In J. Davies and J. Gibbons, editors, Proceedings of the Sixth International Conference on Integrated Formal Methods (IFM), volume 4591 of LNCS, pages 619-638, 2007.


Automated Rail Cars System, Car Platooning


Click here for the binary.


Just type ./ on the command line to see how it can be used.


Proof of Concept