Putting advanced reachability analysis techniques together: The “ARA” tool

  • Antti Valmari
  • Jukka Kemppainen
  • Matthew Clegg
  • Mikko Levanto
Part of the Lecture Notes in Computer Science book series (LNCS, volume 670)


“ARA” is a verification tool which applies some recent improved speed verification techniques. ARA accepts as input systems described in Basic Lotos. With ARA, a system can be verified by showing that it is behaviourally equivalent with its specification. For comparing behaviours, ARA uses a novel CSP-like but catastrophe-free behavioural equivalence notion called “CFFD-equivalence”. ARA can also reduce the behaviour of the system into a small “normal” form, and show the result graphically. ARA applies two techniques to cope with the state explosion problem: compositional LTS construction and the stubborn set method. The paper contains a detailed example of the validation of a communication protocol using ARA. The paper concentrates on the intuition behind the various novel ideas of ARA; formal details are mostly omitted.


Linear Temporal Logic Label Transition System Reachability Analysis Compositional Method Verification Tool 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bergstra, J. A. & Klop, J. W. & Olderog, E.-R.: Failures without Chaos: A New Process Semantics for Fair Abstraction. Formal Description of Programming Concepts III, North-Holland 1987, pp. 77–103.Google Scholar
  2. 2.
    Bochmann, G. v.: Usage of Protocol Development Tools: The Results of a Survey. Proceedings of the 7th International IFIP WG 6.1 Symposium on Protocol Specification, Testing and Verification (1987), North-Holland 1988.Google Scholar
  3. 3.
    Bolognesi, T. & Brinksma, E.: Introduction to the ISO Specification Language LO-TOS. Computer Networks and ISDN Systems 14 1987 pp. 25–59. Also: The Formal Description Technique LOTOS, North-Holland 1989, pp. 23–73.CrossRefGoogle Scholar
  4. 4.
    Brookes, S. D. & Hoare, C. A. R. & Roscoe, A. W.: A Theory of Communicating Sequential Processes. Journal of the ACM 31 (3) 1984 pp. 560–599.CrossRefGoogle Scholar
  5. 5.
    Clarke, E. M. & Emerson, E. A. & Sistla, A. P.: Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, vol 8, 1986, pp. 244–263.CrossRefGoogle Scholar
  6. 6.
    Cleaveland, R. & Parrow, J. & Steffen, B.: The Concurrency Workbench. Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science 407, Springer-Verlag 1990, pp. 24–37.Google Scholar
  7. 7.
    Feldbrugge, F. & Jensen, K.: Petri Net Tool Overview 1986. Advances in Petri Nets 1986, Part II, Lecture Notes in Computer Science 255, Springer-Verlag 1987, pp. 20–61.Google Scholar
  8. 8.
    Fernandez, J.-C: An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming 13 (1989/90) pp. 219–236.CrossRefGoogle Scholar
  9. 9.
    Fernandez, J.-C. & Mounier, L.: A Tool Set for Deciding Behavioural Equivalences. Proceedings of CONCUR '91, Lecture Notes in Computer Science 527, Springer-Verlag 1991, pp. 23–42.Google Scholar
  10. 10.
    Graf, S. & Steffen, B.: Compositional Minimization of Finite-State Processes. In: Computer-Aided Verification '90 (Proceedings of a workshop), AMS DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol 3, American Mathematical Society 1991, pp. 57–73.Google Scholar
  11. 11.
    Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall 1985, 256 p.Google Scholar
  12. 12.
    ISO 8807 International Standard: Information processing systems — Open Systems Interconnection — LOTOS — A formal description technique based on the temporal ordering of observational behaviour. International Organization for Standardization, 1989, 142 p.Google Scholar
  13. 13.
    Kaivola, R. & Valmari, A.: Using Truth-Preserving Reductions to Improve the Clarity of Kripke Models. Proceedings of CONCUR '91, Lecture Notes in Computer Science 527, Springer-Verlag 1991, pp. 361–375.Google Scholar
  14. 14.
    Kaivola, R. & Valmari, A.: The Weakest Compositional Semantic Equivalence Preserving Nexttime-Less Linear Temporal Logic. Proceedings of CONCUR '92, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 207–221.Google Scholar
  15. 15.
    Lichtenstein, O. & Pnueli, A.: Checking that Finite State Concurrent Programs Satisfy their Linear Specification. Tenth ACM Symposium on Principles of Programming Languages, 1984, pp. 97–107.Google Scholar
  16. 16.
    Madelaine, E. & Vergamini, D.: AUTO: A Verification Tool for Distributed Systems Using Reduction of Finite Automata Networks. Formal Description Techniques II (Proceedings of FORTE '89), North-Holland 1990, pp. 61–66.Google Scholar
  17. 17.
    Milner, R.: Communication and Concurrency. Prentice-Hall 1989, 260 p.Google Scholar
  18. 18.
    Petri Net Newsletter 41, Special Volume: Petri Net Tools Overview 92. Gesellschaft für Informatik, Bonn, Germany, April 1992, 43 p.Google Scholar
  19. 19.
    Pnueli, A.: Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends. Current Trends in Concurrency, Lecture Notes in Computer Science 224, Springer-Verlag 1985, pp. 510–584.Google Scholar
  20. 20.
    Valmari, A.: Error Detection by Reduced Reachability Graph Generation. Proceedings of the Ninth European Workshop on Application and Theory of Petri Nets, Venice, Italy 1988, pp. 95–112.Google Scholar
  21. 21.
    Valmari, A.: PC-Rimst — A Tool for Validating Concurrent Program Designs. Micro-processing and Microprogramming 24 (1988) 1–5 (Proceedings of the Euromicro '88), pp. 809–818.Google Scholar
  22. 22.
    Valmari, A.: Stubborn Sets for Reduced State Space Generation. Advances in Petri Nets 1990, Lecture Notes in Computer Science 483, Springer-Verlag 1991, pp. 491–515. (An earlier version appeared in Proceedings of the Tenth International Conference on Application and Theory of Petri Nets, Bonn, FRG 1989, Vol. II pp. 1–22.)Google Scholar
  23. 23.
    Valmari, A.: A Stubborn Attack on State Explosion. Formal Methods is System Design, 1: 297–322 (1992). (Earlier version appeared in Proceedings of the Workshop on Computer-Aided Verification 1990.)CrossRefGoogle Scholar
  24. 24.
    Valmari, A.: Compositional State Space Generation. University of Helsinki, Department of Computer Science, Report A-1991–5, Helsinki, Finland 1991. 30 p. (An earlier version appeared in Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France 1990, pp. 43–62.)Google Scholar
  25. 25.
    Valmari, A. et Clegg, M.: Reduced Labelled Transition Systems Save Verification Effort. Proceedings of CONCUR '91, Lecture Notes in Computer Science 527, Springer-Verlag 1991, pp. 526–540.Google Scholar
  26. 26.
    Valmari, A. & Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm. Protocol Specification, Testing and Verification XI (Proceedings of the 11th International IFIP Symposium), North-Holland 1991, pp. 3–18.Google Scholar
  27. 27.
    Valmari, A.: Alleviating State Explosion during Verification of Behavioural Equivalence. University of Helsinki, Department of Computer Science, Report A-1992-4, Helsinki, Finland 1992. 57 p.Google Scholar
  28. 28.
    Wheeler, G. R. & Valmari, A. & Billington, J.: Baby TORAS Eats Philosophers but Thinks about Solitaire. Proceedings of the Fifth Australian Software Engineering Conference, Sydney, Australia 1990, pp. 283–288.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Antti Valmari
    • 1
  • Jukka Kemppainen
    • 1
  • Matthew Clegg
    • 1
  • Mikko Levanto
    • 1
  1. 1.Computer Technology LaboratoryTechnical Research Centre of FinlandOuluFinland

Personalised recommendations