An Exercise in Protocol Verification

  • Stefania Gnesi
  • Eric Madelaine
  • Gioia Ristori


The word “verification” is used by various people in many different contexts, and with many different meanings. In the area of parallel and concurrent programming, it refers to activities as different as proof of equivalence between two programs, reachability analysis, the checking of logical properties of a program, or even assertion that a program passes a given test set, or generation of random traces by means of simulation. The verification activities we shall consider here are those directly associated with the analysis of a finite model of the behaviour of a system, namely the building and analysis of such a model, proof of equivalence, and model checking.


Model Checker Temporal Logic Label Transition System Kripke Structure 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]
    G. Boudol. Notes on algebraic calculi of processes. In K. Apt, editor, Logics and Models of Concurrent Systems, NATO-ISA series F13, 1985.Google Scholar
  2. [2]
    G. Boudol, V. Roy, R. de Simone, and D. Vergamini. Process calculi from theory to practice: Verification tools. In Proc. of the Workshop on Automated Verification Methods for Finite State Systems, LNCS 407. Springer-Verlag, 1989.Google Scholar
  3. [3]
    M.C. Browne, D. Dill, E.M. Clarke, and B. Mishra. Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, C-35(12):1035–1044, 1986.MATHCrossRefGoogle Scholar
  4. [4]
    E.M. Clarke, E.A. Emerson, A.P. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM Toplas, 8 (2), 1986, pp. 244–263.MATHCrossRefGoogle Scholar
  5. [5]
    R. Cleaveland and B. Steffen. A linear-time model checking algorithm for the alternation-free modal mu-calculus. In 3rd Workshop on Computer-aided Verification, LNCS 575,Aalborg, 1991. Springer-Verlag.Google Scholar
  6. [6]
    R. J. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench. In Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science 407. Springer-Verlag, 1989.Google Scholar
  7. [7]
    R. De Nicola, S. Fantechi, S. Gnesi, and G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems. In 3rd Workshop on Computer-aided Verification, Aalborg, July 1991. Springer-Verlag, and Computer Networks and ISDN Systems, vol. 25, n. 7, 1993.Google Scholar
  8. [8]
    R. De Nicola, F. Vaandrager. Action versus state based logics for transition systems. In I. Guessarian, editor, Proceedings Ecole du Printemps on Semantics of Concurrency. Springer Verlag LNCS 469, 1990.Google Scholar
  9. [9]
    R. De Nicola, F. Vaandrager. Three logics for branching bisimulations. In Proc. of the 5th Annual Symposium on Logic in Computer Science (LICS ’ 90), pages 118–129, Philadelphia, 1990. IEEE Computer Society Press.Google Scholar
  10. [10]
    E. A. Emerson and J. Halpern. “sometime” and “not never” revisited: On branching versus linear time temporal logic“. Journal of ACM, 33:151–178, January 1986.MathSciNetMATHCrossRefGoogle Scholar
  11. [11]
    A. Fantechi, S. Gnesi, G. Ristori. From ACTL to µ-calculus. ERCIM Workshop on Theory and Practice in Verification. Pisa 1992.Google Scholar
  12. [12]
    A. Fantechi, S. Gnesi, G. Ristori. ACTLab: Verifying Concurrent Systems by Talking to Them. First International Conference on Temporal Logic, Bonn, July 11–14 1994.Google Scholar
  13. [13]
    A. Fantechi, G. Ferro, S. Gnesi, G. Ristori. AMC: a Model Checker for ACTL formulae. IEI Technical Report. Pisa 1993.Google Scholar
  14. [14]
    H. Garavel and J. Sifakis. Compilation and verification of Lotos specifications. In proceedings of the 10 th International symposium on Protocol Specification, Testing and Verification, Ottawa, 1990. IFIP, North-Holland.Google Scholar
  15. [15]
    F. Giannotti, D. Latella. Gate Splitting in LOTOS Specifications Using Abstract Interpretation. TAPSOFT 93, LNCS 668.Google Scholar
  16. [16]
    M. Hennessy and H. Lin. Symbolic bisimulations. Technical Report 1/92, University of Sussex, April 1992.Google Scholar
  17. [17]
    M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of ACM, 32(1):137–161, January 1985.MathSciNetMATHCrossRefGoogle Scholar
  18. [18]
    D. Kozen. Results on the propositional n-calculus. Theoretical Computer Science, 27:333–354, 1983.MathSciNetMATHCrossRefGoogle Scholar
  19. [19]
    E. Madelaine. Verification tools from the CONCUR project. Bulletin of the EATCS, 47:110–127, 1992.Google Scholar
  20. [20]
    E. Madelaine and D. Vergamini. Auto: A verification tool for distributed systems using reduction of finite automata networks. In S. T. Vuong, editor, Formal Description Techniques, II, FORTE’89 conference, Vancouver, December 1989. North-Holland.Google Scholar
  21. [21]
    E. Madelaine and D. Vergamini. Finiteness conditions and structural construction of automata for all process algebras. In R. Kurshan, editor, proceedings of Workshop on Computer Aided Verification, New-Brunswick, June 1990. AMS-DIMACS.Google Scholar
  22. [22]
    E. Madelaine and D. Vergamini. Specification and verification of a sliding window protocal in LOTOS. In K. R. Parker and G. A. Rose, editors, Formal Description Techniques, IV, volume C-2 of IFIP Transactions, Sydney, December 1991. North-Holland.Google Scholar
  23. [23]
    E. Najm. A verification oriented specification of the transport protocol. In P.H.J. van Eijk, C.A. Vissers, and M. Diaz, editors, The Formal Description Technique LOTOS. North-Holland, 1989.Google Scholar
  24. [24]
    V. Roy and R. de Simone. Auto and autograph. In R. Kurshan, editor, proceedings of Workshop on Computer Aided Verification, New-Brunswick, June 1990. AMSDIMACS.Google Scholar

Copyright information

© Springer Science+Business Media Dordrecht 1995

Authors and Affiliations

  • Stefania Gnesi
    • 1
  • Eric Madelaine
    • 2
  • Gioia Ristori
    • 3
  1. 1.IEI- CNRItaly
  2. 2.INRIAFrance
  3. 3.University of PisaItaly

Personalised recommendations