Advertisement

A front-end generator for verification tools

  • Rance Cleaveland
  • Eric Madelaine
  • Steve Sims
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1019)

Abstract

This paper describes the Process Algebra Compiler (PAC), a front-end generator for process-algebra-based verification tools. Given descriptions of a process algebra's concrete and abstract syntax and semantics as structural operational rules, the PAC produces syntactic routines and functions for computing the semantics of programs in the algebra. Using this tool greatly simplifies the task of adapting verification tools to the analysis of systems described in different languages; it may therefore be used to achieve source-level compatibility between different verification tools. Although the initial verification tools targeted by the PAC are MAUTO and the Concurrency Workbench, the structure of the PAC caters for the support of other tools as well.

Keywords

Semantic Relation Operational Semantic Recursive Call Label Transition System Process Algebra 
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. [1]
    D. Austry and G. Boudol. Algèbre de processus et synchronisation. Theoretical Computer Science, 30:91–131, 1984.Google Scholar
  2. [2]
    J.C.M. Baeten and C. Verhoef. A congruence theorem for structured operational semantics with predicates. Technical Report 93/05, Eindhoven University of Technology, 1994.Google Scholar
  3. [3]
    G. Bhat, R. Cleaveland, and O. Grumberg. Efficient on-the-fly model checking for CTL*. In Tenth Annual Symposium on Logic in Computer Science (LICS '95), San Diego, July 1995. IEEE Computer Society Press.Google Scholar
  4. [4]
    B. Bloom, S. Istrail, and A. Meyer. Bisimulation can't be traced. In Fifteenth Annual ACM Symposium on Principles of Programming Languages (PoPL '88), pages 229–239, San Diego, January 1988. IEEE Computer Society Press.Google Scholar
  5. [5]
    T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. In P.H.J. van Eijk, C.A.Vissers, and M.Diaz, editors, The Formal Description Technique LOTOS, pages 23–76. North-Holland, 1989.Google Scholar
  6. [6]
    G. Boudol, V. Roy, R. de Simone, and D. Vergamini. Process calculi, from theory to practice: Verification tools. Rapport de Recherche RR.1098, INRIA, October 1989.Google Scholar
  7. [7]
    R. Cleaveland. Analyzing concurrent systems using the Concurrency Workbench. In P.E. Lauer, editor, Functional Programming, Concurrency, Simulation and Automated Reasoning, volume 693 of Lecture Notes in Computer Science, pages 129–144. Springer-Verlag, 1993.Google Scholar
  8. [8]
    R. Cleaveland and M.C.B. Hennessy. Testing equivalence as a bisimulation equivalence. In Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, pages 11–23. Springer-Verlag, 1989.Google Scholar
  9. [9]
    R. Cleaveland and M.C.B. Hennessy. Priorities in process algebra. Information and Computation, 87(1/2):58–77, July/August 1990.Google Scholar
  10. [10]
    R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench: A semantics-based tool for the verification of finite-state systems. ACM Transactions on Programming Languages and Systems, 15(1):36–72, January 1993.Google Scholar
  11. [11]
    J.C. Fernandez. Aldébaran: A tool for verification of communicating processes. Technical Report Spectre-c 14, LGI-IMAG, Grenoble, 1989.Google Scholar
  12. [12]
    J.F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 2(100):202–260, 1992.Google Scholar
  13. [13]
    G. Kahn. Natural semantics. Technical Report RR.601, INRIA, 1987.Google Scholar
  14. [14]
    K.G. Larsen, J.C. Godskesen, and M. Zeeberg. TAV, tools for automatic verification, user manual. Technical Report R 89-19, Dept of Mathematics and Computer Science, Ålborg university, 1989.Google Scholar
  15. [15]
    K.G. Larsen and L. Xinxin. Compositionality through an operational semantics of contexts. In M.S. Paterson, editor, Automata, Languages and Programming (ICALP '90), volume 443 of Lecture Notes in Computer Science, pages 526–539, Warwick, England, July 1990. Springer-Verlag.Google Scholar
  16. [16]
    E. Madelaine, R. de Simone, and D. Vergamini. ECRINS, user manual, 1988. Technical Documentation.Google Scholar
  17. [17]
    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
  18. [18]
    E. Madelaine and D. Vergamini. Specification and verification of a sliding window protocol 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
  19. [19]
    R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  20. [20]
    G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, University of Aarhus, September 1981.Google Scholar
  21. [21]
    V. Roy and R. de Simone. Auto and autograph. In R. Kurshan, editor, proceedings of Workshop on Computer Aided Verification, New-Brunswick, June 1990. AMS-DIMACS.Google Scholar
  22. [22]
    C. Verhoef. A congruence theorem for structured operational semantics with predicates and negative premises. In B. Jonsson and J. Parrow, editors, Proceedings CONCUR. 94, Uppsala, Sweden, volume 836 of Lectures Notes in Computer Science, pages 433–448. Springer-Verlag, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Rance Cleaveland
    • 1
  • Eric Madelaine
    • 2
  • Steve Sims
    • 1
  1. 1.Department of Computer ScienceNorth Carolina State UniversityRaleighUSA
  2. 2.INRIASophia Antipolis CedexFrance

Personalised recommendations