Specification & verification of higher order processes
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.
KeywordsTemporal Logic Inference Rule Specification Language Proof System Liveness Property
Unable to display preview. Download preview PDF.
- 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.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- M. Hennessy and R. Milner, Algebraic Laws for Nondeterminism and Concurrency. JACM, Vol. 32, no. 1 1985, pp. 137–161.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- R. Milner, J. Parrow, and D. Walker, A Calculus of Mobile Processes, Part I. Report no. ECS-LFCS-89-86, Edinburgh University, 1989.Google Scholar
- 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.Google Scholar
- B. Thomsen, A Calculus of Higher-order Communicating Systems. In Proc. POPL'89, ACM Press, 1989, pp. 143–154.Google Scholar
- 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.Google Scholar
- Zhou Chao-Chen, A Temporal Semantics of Communicating Processes. In Proc. of Pan Pacific Computer Conference, Melbourne 1985, pp. 617–630.Google Scholar
- 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.Google Scholar