Subproject

S2

Categories

Model reduction

Overview

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.

Publications

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.

Benchmarks

Automated Rail Cars System, Car Platooning

Download

Click here for the binary.

Manual

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

Status

Proof of Concept