Subproject

S2

Categories

Model reduction

Overview

The tool combines a particular finitary abstraction, namely Data-Type Reduction for Dynamic Communication Systems, with global system invariants obtained by abstract interpretation the model. These system invariants are automatically computed by the tool and establish an over-approximation of possible communication topologies occurring at runtime. The invariants are integrated into the abstraction procedure and thereby identify and exclude spurious behaviour of the finitary abstraction.

Publications

J. Bauer, T. Toben, and B. Westphal. Mind the shapes: Abstraction refinement via topology invariants. In 5th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2007.

J. Bauer, I. Schäfer, T. Toben, and B. Westphal. Specification and verification of dynamic communication systems. In Kees Goossens and Laure Petrucci, editors, Proceedings of the 6th International Conference on Application of Concurrency to System Design (ACSD), 2006.

Benchmarks

Car Platooning

Download

Click here for the binary.

Manual

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

Status

Proof of Concept