Abstract
A system is a collection of processes connected by channels over which they communicate. We consider systems where processes can be communicated. We propose an extension to propositional temporal logic as specification language and an extension to CSP as programming notation for such higher order systems, and we give a sound compositional proof system for verifying that a process satisfies a specification.
Both authors are partially funded by ProCoS ESPRIT BRA 3104.
Partially funded by the Danish Technical Research Council under project RaPiD.
On leave of absence from Institute of Software, Academia Sinica, Beijing, China.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
E. Astesiano, A. Giovini, and G. Reggio, Generalized Bisimulation in Relational Specifications. In STACS 88, R. Cori and M. Wirsing (Eds.), LNCS 294, Springer-Verlag, 1988, pp. 207–226.
G. Boudol, Towards a Lambda-Calculus for Concurrent and Communicating Systems. In TAPSOFT'89, J. Diaz and F. Orejas (Eds.), LNCS 351, Springer-Verlag, 1989, pp. 149–161.
M.R. Hansen and Zhou Chao-Chen, Specification & Verification of Higher Order Processes: A Temporal Logic Based Approach. ProCoS report ID/DTH MRH 2/1, 1990.
M. Hennessy and R. Milner, Algebraic Laws for Nondeterminism and Concurrency. JACM, Vol. 32, no. 1 1985, pp. 137–161.
K.G. Larsen, Proof Systems for Hennessy-Milner Logic with Recursion. In CAAP'88, M. Dauchet and M. Nivat (Eds.), LNCS 299, Springer-Verlag, 1988, pp. 215–230.
Z. Manna and A. Pnueli, The Anchored Version of the Temporal Framework. In REX'88, J.W. de Bakker, W.-P. de Roever, and G. Rozenberg (Eds.), LNCS 354, Springer-Verlag, 1989, pp. 201–284.
R. Milner, J. Parrow, and D. Walker, A Calculus of Mobile Processes, Part I. Report no. ECS-LFCS-89-86, Edinburgh University, 1989.
F. Nielson, The Typed λ-Calculus with First-Class Processes. In PARLE'89, E. Odijk, M. Rem, and J.-C. Syre (Eds.), LNCS 366, Springer-Verlag, 1989, pp. 357–373.
B. Thomsen, A Calculus of Higher-order Communicating Systems. In Proc. POPL'89, ACM Press, 1989, pp. 143–154.
G. Winskel, A Complete Proof System for SCCS with Modal Assertions. FST and TCS'85, S.N. Maheshwari (Ed.), LNCS 206, Springer-Verlag, 1985, pp. 392–410.
Zhou Chao-Chen, A Temporal Semantics of Communicating Processes. In Proc. of Pan Pacific Computer Conference, Melbourne 1985, pp. 617–630.
Zhou Chao-Chen, Specifying Communicating Systems with Temporal Logic. In Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli (Eds.), LNCS 398, Springer-Verlag, 1989, pp. 304–323.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hansen, M.R., Zhou, CC. (1990). Specification & verification of higher order processes. In: Rovan, B. (eds) Mathematical Foundations of Computer Science 1990. MFCS 1990. Lecture Notes in Computer Science, vol 452. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0029625
Download citation
DOI: https://doi.org/10.1007/BFb0029625
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52953-8
Online ISBN: 978-3-540-47185-1
eBook Packages: Springer Book Archive