Testing equivalence for mobile processes

  • Michele Boreale
  • Rocco De Nicola
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


The impact of applying the testing approach to a calculus of processes with a dynamically changing structure is investigated. A proof system for the finite fragment of the calculus is introduced which consists of two groups of laws: those for strong observational equivalence and those needed to deal with τ actions. Soundness and completeness w.r.t. a testing preorder are shown. A fully abstract denotational model for the language is presented which relies on the existence of normal forms for processes.


Normal Form Inference Rule Operational Semantic Proof System Process Algebra 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BK89]
    Bergstra,J.A. and Klop,J.-W. Process Theory based on Bisimulation Semantics, in Linear Time, Branching Time and Partial Orders in Logic and Models for Concurrency, LNCS, 354, Springer-Verlag, 1989, 50–122.Google Scholar
  2. [Bor91]
    Boreale,M. Semantica osservazionale ed assiomatica per un'algebra di processi dinamici, Master Thesis, Università di Pisa, February, 1991.Google Scholar
  3. [DH84]
    De Nicola,R. and Hennessy,M. Testing Equivalence for Processes, Theoret. Comput. Sci., 34 (1984), 83–133.zbMATHMathSciNetCrossRefGoogle Scholar
  4. [DeN87]
    De Nicola,R. Extensional Equivalences for Transition Systems, Acta Informatica, 24, 1987, pp. 211–237.zbMATHMathSciNetCrossRefGoogle Scholar
  5. [DIN90]
    De Nicola,R., Inverardi,P. and Nesi,M. Using Axiomatic Presentation of Behavioural Equivalences for Manipulating CCS Specifications. In Automatic Verification Methods for Finite State Machines (J. Sifakis, ed.) LNCS 407, 1990; pp. 54–67.Google Scholar
  6. [EN86]
    Engberg,U. and Nielsen,M. A Calculus of Communicating Systems with Label Passing; Int. Rep. Computer Science Dept., Aarhus University, DAIMI-PB 208,1986.Google Scholar
  7. [Gue81]
    Guessarian,I. Algebraic Semantics, LNCS, 99, 1981Google Scholar
  8. [Hen88]
    Hennessy,M. An Algebraic Theory of Processes, MIT Press, Cambridge, 1988.Google Scholar
  9. [Hen91]
    Hennessy,M. A Model for the π-Calculus, Internal Report No 8/91, Computer Science, University of Sussex, 1991.Google Scholar
  10. [HI91]
    Hennessy,M. and Ingolfsdottir,A,. A Theory of Testing Equivalence with Value-passing, to appear in Information and Computation, 1991Google Scholar
  11. [Hoa85]
    Hoare,C.A.R. Communicating Sequential Process, Prentice Hall Int., London 1985.Google Scholar
  12. [HP80]
    Hennessy,M. and Plotkin,G. A Term Model for CCS, LNCS, 88, Springer-Verlag, 1980Google Scholar
  13. [Hui92]
    Huimin L., Pam: A Process Algebra Manipulator, in Computer Aided Verification(K.G. Larsen and A. Skou, eds) LNCS 575,1992.Google Scholar
  14. [Mil80]
    Milner,R. A Calculus of Communicating Systems. LNCS, 92, Springer-Verlag, 1980.Google Scholar
  15. [Mil89]
    Milner,R. Communicating and Concurrency. Prentice Hall Int., London 1989.Google Scholar
  16. [MPW89]
    Milner,R., Parrow,J. and Walker,D. A Calculus of Mobile Processes part I and II, LFCS Report Series, Department of Computer Science, University of Edinburgh, 1989. To appear in Information and Computation.Google Scholar
  17. [Plo81]
    Plotkin, G. A Structural Approach to Operational Semantics. Technical Report Computer Science Department, Aarhus University, DAIMI FN-19; 1981).Google Scholar
  18. [Tho91]
    Thomsen,B A Calculus of Higher Order, Proc. of POPL 1989; ACM 1989; pp. 143–154.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Michele Boreale
    • 1
  • Rocco De Nicola
    • 1
  1. 1.Dipartimento di Scienze dell'InformazioneUniversità di Roma “La Sapienza”RomaItaly

Personalised recommendations