RESY: Requirement Synthesis for Compositional Model Checking

Current version: 1.6
Copyright © 2007 Saarland University

Introduction

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.

Industrial Partner

RESY was developed in cooperation with our industrial partner META-LEVEL Software AG.

Operation Modes

• 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

Download

You can download and use RESY under the terms of the following LICENSE.

Contact

For bug reports please contact Hans-Jörg Peter.