RESY: Requirement Synthesis for Compositional Model Checking

  • Bernd Finkbeiner
  • Hans-Jörg Peter
  • Sven Schewe
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


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.


  1. 1.
    Giannakopoulou, D., Păsăreanu, C.S., Barringer, H.: Assumption generation for software component verification. In: Proc. ASE, pp. 3–12. IEEE Computer Society, Los Alamitos (2002)Google Scholar
  2. 2.
    Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2–13. Springer, Heidelberg (2001)Google Scholar
  3. 3.
    Alur, R., Madhusudan, P., Nam, W.: Symbolic compositional verification by learning assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 548–562. Springer, Heidelberg (2005)Google Scholar
  4. 4.
    Finkbeiner, B., Schewe, S., Brill, M.: Automatic synthesis of assumptions for compositional model checking. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 143–158. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Holzmann, G.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Bernd Finkbeiner
    • 1
  • Hans-Jörg Peter
    • 1
  • Sven Schewe
    • 1
  1. 1.Universität des SaarlandesSaarbrückenGermany

Personalised recommendations