Advertisement

Verifying Liveness by Augmented Abstraction

  • Yonit Kesten
  • Amir Pnueli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1683)

Abstract

The paper deals with the proof method of verification by augmented finitary abstraction (VAA), which presents an effective approach to the verification of the temporal properties of (potentially infinitestate) reactive systems. The method consists of a two-step process by which, in a first step, the system and its temporal specification are combined an then abstracted into a finite-state Büchi automaton. The second step uses model checking to establish emptiness of the abstracted automaton.

The (VAA) method can be considered as a viable alternative to verification by temporal deduction which, up to now, has been the main method shown to be complete for the verification of infinite-state systems.

The paper presents a general recipe for the abstraction of Büchi automata which is shown to be sound, where soundness means that emptiness of the abstract automaton implies emptiness of the concrete (infinitestate) automaton. To make the method applicable for the verification of liveness properties, pure abstraction is sometimes no longer adequate.We show that by augmenting the system by an appropriate (and standardly constructible) progress monitor, we obtain an augmented system, whose computations are essentially the same as the original system, and which may now be abstracted while preserving the desired liveness properties. We then proceed to show that the (VAA) method is sound and complete for proving all properties expressible by temporal logic (including both safety and liveness). Completeness establishes that whenever an infinite-state Büchi automaton has no computations, there exists a finitary abstraction which abstracts the automaton, augmented by an appropriate progress monitor, into a finite-state Büchi automaton with no computations

Keywords

Model Check Temporal Property Ranking Function Linear Temporal Logic Augmented System 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BBLS92]
    S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Properties preserving simulations. CAV’92, LNCS 663.Google Scholar
  2. [BBM95]
    N. Bjørner, I.A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. In 1st Intl. Conf. on Principles and Practice of Constraint Programming, LNCS 967, 1995.Google Scholar
  3. [BLO98]
    S. Bensalem, Y. Lakhnech, and S. Owre. Abstractions of infinite state systems compositionally and automatically. CAV’98, LNCS 1427.Google Scholar
  4. [BMS95]
    I.A. Browne, Z. Manna, and H.B. Sipma. Generalized verification diagrams. In FSTTSC’95, LNCS 1026.Google Scholar
  5. [CC77]
    P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. POPL’77.Google Scholar
  6. [CGH94]
    E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at ltl model checking. CAV’94, LNCS 818.Google Scholar
  7. [CGL94]
    E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Trans. Prog. Lang. Sys., 16(5):1512–1542, 1994.CrossRefGoogle Scholar
  8. [CGL96]
    E.M. Clarke, O. Grumberg, and D.E. Long. Model checking. In Model Checking, Abstraction and Composition, volume 152 of Nato ASI Series F, pages 477–498. Springer-Verlag, 1996.Google Scholar
  9. [CH78]
    P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. POPL’78.Google Scholar
  10. [DGG97]
    D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. Prog. Lang. Sys., 19(2), 1997.Google Scholar
  11. [GFMdR85]
    O. Grumberg, N. Francez, J.A. Makowski, and W.-P. de Roever. A proof rule for fair termination. Inf. and Comp., 66:83–101, 1985.MathSciNetzbMATHGoogle Scholar
  12. [GL93]
    S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. CAV’93, LNCS 697.Google Scholar
  13. [KP98]
    Y. Kesten and A. Pnueli. Deductive verification of fair discrete systems. Technical report, the Weizmann Institute, 1998.Google Scholar
  14. [KP98b]
    Y. Kesten and A. Pnueli. Modularization and Abstraction: The Keys to Formal Verification. MFCS’98, LNCS 1450.Google Scholar
  15. [KPR98]
    Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. ICALP’98, LNCS 1443.Google Scholar
  16. [LP85]
    O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. POPL’85.Google Scholar
  17. [LPS81]
    D. Lehmann, A. Pnueli, and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. In ICALP’81, LNCS 115.Google Scholar
  18. [MAB+94]
    Z. Manna, A. Anuchitanukul, N. Bjørner, A. Browne, E. Chang, M. Colon, L. De Alfaro, H. Devarajan, H. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, 1994.Google Scholar
  19. [MBSU98]
    Z. Manna, A. Brown, H. B. Sipma, and T. E. Uribe. Visual abstractions for temporal verification. AMAST’98.Google Scholar
  20. [MP91a]
    Z. Manna and A. Pnueli. Completing the temporal picture. Theor. Comp. Sci., 83(1):97–130, 1991.CrossRefGoogle Scholar
  21. [MP91b]
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.zbMATHGoogle Scholar
  22. [MP94]
    Z. Manna and A. Pnueli. Temporal verification diagrams. In Theoretical Aspects of Computer Software, LNCS 789, 1994.CrossRefGoogle Scholar
  23. [MP95]
    Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.CrossRefGoogle Scholar
  24. [SUM96]
    H.B. Sipma, T.E. Uribe, and Z. Manna. Deductive model checking. CAV’96.Google Scholar
  25. [Uri99]
    T. E. Uribe. Abstraction-Based Deductive-Algorithmic Verification of Reactive Systems. PhD thesis, Stanford University, 1999.Google Scholar
  26. [Var91]
    M. Y. Vardi. Verification of concurrent programs-the automata-theoretic framework. Annals of Pure Applied Logic, 51:79–98, 1991.MathSciNetCrossRefGoogle Scholar
  27. [VW86]
    M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS’86.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Yonit Kesten
  • Amir Pnueli

There are no affiliations available

Personalised recommendations