Advertisement

Abstraction and Modular Verification of Infinite-State Reactive Systems

  • Zohar Manna
  • Michael A. Colón
  • Bernd Finkbeiner
  • Henny B. Sipma
  • Tomás E. Uribe
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1526)

Abstract

We review a number of temporal verification techniques for reactive systems using modularity and abstraction. Their use allows the verification of larger systems, and the incremental verification of systems as they are developed and refined. In particular, we show how deductive verification tools, and the combination of finite-state model checking and abstraction, allow the verification of infinite-state systems featuring data types commonly used in software specifications, including real-time and hybrid systems.

Keywords

Model Check Hybrid System Temporal Logic Transition Relation Mutual Exclusion 
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. [ABL96]
    Abrial, J.R., Boerger, E., Langmaack, H. (eds.): Dagstuhl Seminar 1995. LNCS, vol. 1165. Springer, Heidelberg (1996)zbMATHGoogle Scholar
  2. [AHS96]
    Alur, R., Henzinger, T.A., Sontag, E.D. (eds.): HS 1995. LNCS, vol. 1066. Springer, Heidelberg (1996)Google Scholar
  3. [BBC+95]
    Bjørner, N.S., Browne, A., Chang, E.S., Colón, M., Kapur, A., Manna, Z., Sipma, H.B., Uribe, T.E.: STeP: The Stanford Temporal Prover, User’s Manual. Technical Report STAN-CS-TR-95-1562, Computer Science Department, Stanford University (November 1995)Google Scholar
  4. [BBC+96]
    Bjørner, N.S., Browne, A., Chang, E.S., Colón, M., Kapur, A., Manna, Z., Sipma, H.B., Uribe, T.E.: STeP: Deductive-algorithmic verification of reactive and real-time systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 415–418. Springer, Heidelberg (1996)Google Scholar
  5. [BBM97]
    Bjørner, N.S., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theoretical Computer Science 173(1), 49–87 (1997); Preliminary version aqppeared in Montanari, U., Rossi, F. (eds.): CP 1995. LNCS, vol. 976, pp. 589–623. Springer, Heidelberg (1995)Google Scholar
  6. [BLM97]
    Bjørner, N.S., Lerner, U., Manna, Z.: Deductive verification of parameterized fault-tolerant systems: A case study. In: Intl. Conf. on Temporal Logic. Kluwer, Dordrecht (1997) (to appear)Google Scholar
  7. [BLO98]
    Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 319–331. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  8. [BMS95]
    Browne, A., Manna, Z., Sipma, H.B.: Generalized temporal verification diagrams. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 484–498. Springer, Heidelberg (1995)Google Scholar
  9. [BMSU97]
    Bjørner, N.S., Manna, Z., Sipma, H.B., Uribe, T.E.: Deductive verification of real-time systems using STeP. In: Rus, T., Bertrán, M. (eds.) AMAST-ARTS 1997, ARTS 1997, and AMAST-WS 1997. LNCS, vol. 1231, pp. 22–43. Springer, Heidelberg (1997)Google Scholar
  10. [CC77]
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fix-points. In: 4th ACM Symp. Princ. of Prog. Lang., pp. 238–252. ACM Press, New York (1977)Google Scholar
  11. [CE81]
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. IBM Workshop on Logics of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)Google Scholar
  12. [CGL94]
    Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. on Programming Languages and Systems 16(5), 1512–1542 (1994)CrossRefGoogle Scholar
  13. [CU98]
    Colón, M.A., Uribe, T.E.: Generating finite-state abstractions of reactive systems using decision procedures. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 293–304. Springer, Heidelberg (1998)Google Scholar
  14. [Dam96]
    Dams, D.R.: Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology (July 1996)Google Scholar
  15. [dBdRR90]
    de Bakker, J.W., de Roever, W.P., Rosenberg, G. (eds.): REX 1989. LNCS, vol. 430. Springer, Heidelberg (1990)Google Scholar
  16. [DGG94]
    Dams, D.R., Grümberg, O., Gerth, R.: Abstract interpretation of reactive systems: Abstractions preserving VCTL*, 3ECTL*, CTL*. In: IFIP Working Conference on Programming Concepts, Methods and Calculi (PRO-COMET 1994), pp. 573–592 (June 1994)Google Scholar
  17. [DGH95]
    Damm, W., Grümberg, O., Hungar, H.: What if model checking must be truly symbolic. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 230–244. Springer, Heidelberg (1995)Google Scholar
  18. [DKRT97]
    D’Argenio, P.R., Katoen, J.P., Ruys, T., Tretmans, G.T.: The bounded retransmission protocol must be on time! In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 416–432. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  19. [DOTY96]
    Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool krones. In: Alur, et al. (eds.) [AHS96], pp. 208–219 (1996)Google Scholar
  20. [FMS98]
    Finkbeiner, B., Manna, Z., Sipma, H.B.: Deductive verification of modular systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, p. 239. Springer, Heidelberg (1998) (to appear)Google Scholar
  21. [GS97]
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)Google Scholar
  22. [HH95]
    Henzinger, T.A., Ho, P.: HyTech: The Cornell hybrid technology tool. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999, pp. 265–293. Springer, Heidelberg (1995)Google Scholar
  23. [HLP98]
    Havelund, K., Lowry, M., Penix, J.: Formal verification of a space craft controller. Technical report, NASA Ames Research Center (1998)Google Scholar
  24. [HS96]
    Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 662–681. Springer, Heidelberg (1996)Google Scholar
  25. [JW96]
    Jackson, D., Wing, J.: Lightweight formal methods. IEEE Computer (April 1996)Google Scholar
  26. [KMP94]
    Kesten, Y., Manna, Z., Pnueli, A.: Temporal verification of simulation and refinement. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) REX 1993. LNCS, vol. 803, pp. 273–346. Springer, Heidelberg (1994)Google Scholar
  27. [KMP96]
    Kesten, Y., Manna, Z., Pnueli, A.: Verifying clocked transition systems. In: Alur, et al. (eds.) [AHS96], pp. 13–40 (1996)Google Scholar
  28. [LGS+95]
    Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design 6, 1–35 (1995)CrossRefGoogle Scholar
  29. [Lon93]
    Long, D.E.: Model Checking, Abstraction, and Compositional Verification. PhD thesis, School of Computer Science, Carnegie-Mellon University, Pittsburgh, PA (July 1993)Google Scholar
  30. [MBB+98]
    Manna, Z., Bjørner, N.S., Browne, A., Colón, M., Finkbeiner, B., Pichora, M., Sipma, H.B., Uribe, T.E.: An update on STeP: Deductive-algorithmic verification of reactive systems. Tool Support for System Specification, Development and Verification, Christian-Albrechts-Universitat, Kiel, June 1998, 87–91 (1998); Bericht Nr. 9803Google Scholar
  31. [McM93]
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Pub., Dordrecht (1993)zbMATHGoogle Scholar
  32. [MP94]
    Manna, Z., Pnueli, A.: Temporal verification diagrams. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 726–765. Springer, Heidelberg (1994)Google Scholar
  33. [MP95]
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)Google Scholar
  34. [MP96]
    Manna, Z., Pnueli, A.: Clocked transition systems. Technical Report STAN-CS-TR-96-1566, Computer Science Department, Stanford University (April 1996)Google Scholar
  35. [MS98]
    Manna, Z., Sipma, H.B.: Deductive verification of hybrid systems using STeP. In: Henzinger, T., Sastry, S. (eds.) HSCC 1998. LNCS, vol. 1386, pp. 305–318. Springer, Heidelberg (1998)Google Scholar
  36. [Pnu77]
    Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. Found. of Comp. Sci., pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)Google Scholar
  37. [QS82]
    Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)Google Scholar
  38. [SUM98]
    Sipma, H.B., Uribe, T.E., Manna, Z.: Deductive model checking. To appear in Formal Methods in System Design (1998); Preliminary version appeared in Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 208–219. Springer, Heidelberg (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Zohar Manna
    • 1
  • Michael A. Colón
    • 1
  • Bernd Finkbeiner
    • 1
  • Henny B. Sipma
    • 1
  • Tomás E. Uribe
    • 1
  1. 1.Computer Science DepartmentStanford UniversityStanford

Personalised recommendations