RESY: Requirement Synthesis for Compositional Model Checking
Current version: 1.6
Copyright © 2007 Saarland University
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.
RESY was developed in cooperation with our industrial partner META-LEVEL Software AG.
- Assumption generation
resy -M M1,M2,… -E E1,E2,… [-G …] -o out.pro input.pro
- Compositional model checking
resy -M M1,M2,… -E E1,E2,… [-G …] -e input.pro
- SPIN front-end
resy -M M1,M2,… -E E1,E2,… [-G …] -m 0.1 -o out.pro input.pro
- Educational mode
resy -M M1,M2,… -E E1,E2,… [-G …] -vst -dr .dots -o out.pro input.pro
For bug reports please contact Hans-Jörg Peter.