Specification & verification of higher order processes

  • Michael R. Hansen
  • Zhou Chao-Chen 
Part of the Lecture Notes in Computer Science book series (LNCS, volume 452)


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.


Temporal Logic Inference Rule Specification Language Proof System Liveness Property 
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.


  1. [1]
    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
  2. [2]
    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
  3. [3]
    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
  4. [4]
    M. Hennessy and R. Milner, Algebraic Laws for Nondeterminism and Concurrency. JACM, Vol. 32, no. 1 1985, pp. 137–161.Google Scholar
  5. [5]
    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
  6. [6]
    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
  7. [7]
    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
  8. [8]
    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
  9. [9]
    B. Thomsen, A Calculus of Higher-order Communicating Systems. In Proc. POPL'89, ACM Press, 1989, pp. 143–154.Google Scholar
  10. [10]
    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
  11. [11]
    Zhou Chao-Chen, A Temporal Semantics of Communicating Processes. In Proc. of Pan Pacific Computer Conference, Melbourne 1985, pp. 617–630.Google Scholar
  12. [12]
    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

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Michael R. Hansen
    • 1
  • Zhou Chao-Chen 
    • 1
  1. 1.Department of Computer ScienceTechnical University of DenmarkLyngby

Personalised recommendations