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.
This work is partially funded by NSF-INRIA collaboration # CCR-9247478, ES-PRIT Basic Research Action CONCUR2, NSF/DARPA grant CCR-9014775, ONR Young Investigator Award N00014-92-J-1582, and NSF Young Investigator Award CCR-9257963.
Chapter PDF
Similar content being viewed by others
Keywords
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
D. Austry and G. Boudol. Algèbre de processus et synchronisation. Theoretical Computer Science, 30:91–131, 1984.
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.
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.
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.
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.
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.
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.
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.
R. Cleaveland and M.C.B. Hennessy. Priorities in process algebra. Information and Computation, 87(1/2):58–77, July/August 1990.
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.
J.C. Fernandez. Aldébaran: A tool for verification of communicating processes. Technical Report Spectre-c 14, LGI-IMAG, Grenoble, 1989.
J.F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 2(100):202–260, 1992.
G. Kahn. Natural semantics. Technical Report RR.601, INRIA, 1987.
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.
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.
E. Madelaine, R. de Simone, and D. Vergamini. ECRINS, user manual, 1988. Technical Documentation.
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.
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.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, University of Aarhus, September 1981.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cleaveland, R., Madelaine, E., Sims, S. (1995). A front-end generator for verification tools. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1995. Lecture Notes in Computer Science, vol 1019. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60630-0_8
Download citation
DOI: https://doi.org/10.1007/3-540-60630-0_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60630-7
Online ISBN: 978-3-540-48509-4
eBook Packages: Springer Book Archive