Abstract
In this paper, we present a formal verification framework for higher-order value-passing process algebra. This framework stems from an established synergy between type inference and model-checking. The language considered here is based on a sugared version of an implicitly typed λ-calculus extended with higher-order synchronous concurrency primitives. First, we endow such a syntax with a semantic theory made of a static semantics together with a dynamic semantics. The static semantics consists of an annotated type system. The dynamic semantics is operational and comes as a two-layered labeled transition system. The dynamic semantics is abstracted into a transitional semantics so as to make finite some infinite-state processes. We describe the syntax and the semantics of a verification logic that allows one to specify properties. The logic is an extension of the modal µ-calculus for handling higher-order processes, value-passing and return of results.
This research has been funded by a grant from FCAR (Fonds pour la Formation de Chercheurs et l’Aide la Recherche), Quebec, Canada.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. M. Amadio and M. Dam. Reasoning about higher-order processes. In Proc. of CAAP’95, Aarhus, Lecture Notes in Computer Science, 915, 1995.
B. Berthomieu. Implementing CCS, the LCS experiment. Technical Report 89425, LAAS CNRS, 1989.
D. Bolignano and M. Debbabi. A coherent type inference system for a concur-rent, functional and imperative programming language. In Proceedings of the AMAST’93 Conference. Springer Verlag, June 1993.
D. Bolignano and M. Debbabi. A semantic theory for CML. In Proceedings of the TACS’94 Conference. Springer Verlag, April1994.
R. Cridlig. Semantic analysis of shared-memory concurrent languages using ab-stract model-checking. In Symposium on Partial Evaluation and Program Manipulation, 1995.
R. Cridlig. Semantic analysis of concurrent ML by abstract model-checking. In International Workshop on Verification of Infinite State Systems, 1996.
Mads Dam. Model checking mobile processes. Information and Computation, 129(1):35–51, 25 August 1996.
M. Debbabi. Intégration des paradigmes de programmation parallèle, fonctionnelle et impérative: fondements sémantiques. PhD thesis, Université Paris Sud, Centre d’Orsay, July1994.
E. Allen Emerson and Chin-Laung Lei. Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In Proceedings, Symposium on Logic in Computer Science, pages 267–278, Cambridge, Massachusetts, 16–18 June 1986. IEEE Computer Society.
William Ferreira, Matthew Hennessy, and Alan Jeffrey. A theory of weak bisim-ulation for core CML. ACM SIGPLAN Notices, 31(6):201–212, June 1996.
A. Giacalone, P. Mishra, and S. Prasad. Facile: A symmetric integration of concur-rent and functional programming. International Journal of Parallel Programming, 18(2):121–160, April 1989.
K. Havelund and K. G. Larsen. The fork calculus. In A. Lingas, R. Karlsson, and S. Carlsson, editors, Proceedings 20 th ICALP, volume 700 of Lecture Notes in Computer Science. Springer Verlag, 1993.
M. Hennessy and A. Ingólfsdóttir. A theory of communicating processes with value passing. In Proc. 17th ICALP, LNCS. Springer Verlag, 1990.
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 23, 1983.
R. Milner. The polyadic π-calculus: A tutorial. Technical report, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1991.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. Technical report, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1989.
Flemming Nielson and Hanne Riis Nielsen. From CML to process algebra. In E. Best, editor, Proceedings of CONCUR’93, LNCS 715, pages 493–508. Springer-Verlag, 1993.
Hanne Riis Nielson and Flemming Nielson. Higher-order concurrent programs with finite communication topology. In Conference Record of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’94), pages 84–97, Portland, Oregon, January 17–21, 1994. ACM Press. Extended abstract.
J.H. Reppy. Concurrent programming with events-the Concurrent ML manual. Technical report, Department of Computer Science, Cornell University, November 1990.
J.H. Reppy. CML: A higher-order concurrent language. In Proceedings of the ACM SIGPLAN’ 91 PLDI, pages 294–305. SIGPLAN Notices 26(6), 1991.
D.A. Schmidt. Natural-semantics-based abstract interpretation. In Proc. 2d Static Analysis Symposium, Glasgow, Sept. 1995, Lecture Notes in Computer Science 983, pages 1–18. Springer-Verlag, Berlin, 1995.
D.A. Schmidt. Abstract interpretation of small-step semantics. In Proc. 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, Stockholm, June 1996, Lecture Notes in Computer Science 1192, pages 76–99. Springer-Verlag, Berlin, 1997.
Bent Thomsen. A calculus of higher order communicating systems. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, pages 143–154, Austin, Texas, January 1989.
Bent Thomsen. Plain CHOCS. A second generation calculus for higher order processes. Acta Informatica, 30, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Debbabi, M., Benzakour, A., Ktari, B. (1998). A Synergy Between Model-Checking and Type Inference for the Verification of Value-Passing Higher-Order Processes. In: Haeberer, A.M. (eds) Algebraic Methodology and Software Technology. AMAST 1999. Lecture Notes in Computer Science, vol 1548. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49253-4_17
Download citation
DOI: https://doi.org/10.1007/3-540-49253-4_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65462-9
Online ISBN: 978-3-540-49253-5
eBook Packages: Springer Book Archive