RESY - Requirement Synthesis for Compositional Model Checking
Subproject |
S1 |
Categories |
Model reduction |
Overview |
The requirement synthesis tool RESY automatically computes environment assumptions for compositional model checking. Given a process M in a multi-process PROMELA program, an abstraction refinement loop computes a coarse equivalence relation on the states of the environment, collapsing two states if the environment of M can either force the occurrence of an error from both states or from neither state. RESY supports three different operation modes: assumption generation, compositional model checking, and front-end to the model checker SPIN. In assumption generation mode, RESY minimizes the size of the assumption; small assumptions are useful for program documentation and as certificates for re-verification. In compositional model checking mode, RESY terminates as soon as the property is proven or disproven, independently of the size of the assumption. In front-end mode, RESY terminates when the size of the assumption falls below a specified threshold, and calls SPIN with the simplified verification problem. |
B. Finkbeiner, H.-J. Peter, and S. Schewe. Synthesising certificates in networks of timed automata. Institute of Engineering and Technology (IET) Software, 4(3):222-235, June 2010. B. Finkbeiner, H.-J. Peter, and S. Schewe. Synthesizing certificates in networks of timed automata. In 29th IEEE Real-Time Systems Symposium (RTSS), pages 183-194, 2008. B. Finkbeiner, H.-J. Peter, and S. Schewe. RESY: Requirement synthesis for compositional model checking. In C.R. Ramakrishnan and Jakob Rehof, editors, Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of Lecture Notes in Computer Science (LNCS), pages 463-466, 2008. |
|
Production Cell, Sliding Window |
|
Download |
|
Manual |
|
Status |
Stable |