Advertisement

A constraint oriented proof methodology based on modal transition systems

  • Kim G. Larsen
  • Bernhard Steffen
  • Carsten Weise
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1019)

Abstract

We present a constraint-oriented state-based proof methodology for concurrent software systems which exploits compositionality and abstraction for the reduction of the verification problem under investigation. Formal basis for this methodology are Modal Transition Systems allowing loose state-based specifications, which can be refined by successively adding constraints. Key concepts of our method are projective views, separation of proof obligations, Skolemization and abstraction. Central to the method is the use of Parametrized Modal Transition Systems. The method easily transfers to real-time systems, where the main problem are parameters in timing constraints.

Keywords

Transition System Parallel Composition Label Transition System Proof Obligation Memory Component 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [ASW94]
    H. Andersen, C. Stirling, G. Winskel. A Compositional Proof System for the Modal Mu-Calculus. in: Proc. LICS 1994.Google Scholar
  2. [AD94]
    R. Alur, D.L. Dill. A Theory of Timed Automata. in: Theoretical Computer Science Vol. 126, No. 2, April 1994, pp. 183–236.Google Scholar
  3. [AHV93]
    R. Alur, T.A. Henzinger, M.Y. Vardi. Parametric real-time reasoning. Proc. 25th STOC, ACM Press 1993, pp. 592–601.Google Scholar
  4. [BL93]
    M. Broy, L. Lamport. Specification Problem. Case study for the Dagstuhl Seminar 9439, 1994.Google Scholar
  5. [Br86]
    R. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. in: IEEE Transactions on Computation, 35 (8). 1986.Google Scholar
  6. [BCMDH90]
    J. Burch, E. Clarke, K. McMillan, D. Dill, L. Hwang. Symbolic Model Checking: 1020 States and Beyond. in: Proc. LICS'90.Google Scholar
  7. [BS90]
    J. Bradfield, C.Stirling. Local Model Checking for Finite State Spaces. LFCS Report Series ECS-LFCS-90-115, June 1990Google Scholar
  8. [CES83]
    E. Clarke, E.A. Emerson, A.P. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications: A Practical Approach. In Proc. 10th POPL'83Google Scholar
  9. [CGL93]
    K. Čerāns, J.C. Godesken, K.G. Larsen. Timed Modal Specification — Theory and Tools. in: C. Courcoubetis (Ed.), Proc. 5th CAV, 1993. LNCS 697, Springer Berlin 1993, pp. 253–267.Google Scholar
  10. [CGL92]
    E. Clarke, O. Grumber, D. Long. Model Checking and Abstraction. in: Proc. XIX POPL'92.Google Scholar
  11. [CLM89]
    E. Clarke, D. Long, K. McMillan. Compositional Model Checking, in: Proc. LICS'89.Google Scholar
  12. [CC77]
    P. Cousot, R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. in: Proc. POPL'77.Google Scholar
  13. [EFT91]
    R. Enders, T. Filkorn, D. Taubner. Generating BDDs for Symbolic Model Checking in CCS. in: Proceedings CAV'91, LNCS 575, 1991, pp. 203–213Google Scholar
  14. [EL86]
    E. Emerson, J. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proc. LICS'86, pp. 267–278.Google Scholar
  15. [GW91]
    P. Godefroid, P. Wolper. Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. in: Proc. CAV'91, LNCS 575, pp. 332–342.Google Scholar
  16. [GP93]
    P. Godefroid, D. Pirottin. Refining Dependencies Improves Partial-Order Verification Methods. in: Proceedings CAV'93, LNCS 697, 1991, pp. 438–449.Google Scholar
  17. [GL93]
    S. Graf, C. Loiseaux. Program Verification using Compositional Abstraction. in: Proceedings FASE/TAPSOFT'93.Google Scholar
  18. [GS90]
    S. Graf, B. Steffen. Using Interface Specifications for Compositional Minimization of Finite State Systems. in: Proc. CAV'90.Google Scholar
  19. [Koz83]
    D. Kozen. Results on the Propositional mu-Calculus. TCS 27, 333–354, 1983Google Scholar
  20. [HL89]
    H. Hüttel and K. Larsen. The use of static constructs in a modal process logic. Proceedings of Logic at Botik'89. LNCS 363, 1989.Google Scholar
  21. [Lar90]
    K.G. Larsen. Modal specifications. In: Automatic Verification Methods for Finite State Systems LNCS 407, 1990.Google Scholar
  22. [LT88]
    K. Larsen and B. Thomsen. A modal process logic. In: Proceedings LICS'88, 1988.Google Scholar
  23. [Mil89]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  24. [Par81]
    D. Park. Concurrency and automata on infinite sequences. In P. Deussen (ed.), LNCS 104, pp. 167–183, 1981.Google Scholar
  25. [Ste89]
    B. Steffen. Characteristic Formulae. In Proc. ICALP'89, LNCS 372, 1989Google Scholar
  26. [Ste93]
    B. Steffen. Generating data flow analysis algorithms from modal specifications. in: Science of Computer Programming 21, (1993), 115–139.Google Scholar
  27. [Val93]
    A. Valmari. On-The-Fly Verification with Stubborn Sets. in: C. Courcoubetis (Ed.), Proc. 5th CAV, 1993. LNCS 697, pp. 397–408.Google Scholar
  28. [Yi91]
    W. Yi. CCS+Time=an Interleaving Model for Real-Time Systems, Proc. 18th Int. Coll. on Automata, Languages and Programming (ICALP), Madrid, July 1991. LNCS 510, Springer New York 1991, pp. 217–228.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Kim G. Larsen
    • 1
  • Bernhard Steffen
    • 2
  • Carsten Weise
    • 3
  1. 1.BRICSUniversity of AalborgDenmark
  2. 2.University of PassauGermany
  3. 3.University of Technology AachenGermany

Personalised recommendations