Advertisement

Characterizing Termination in LOTOS via Testing

  • David de Frutos
  • Manuel Múñez
  • Juan Quemada
Chapter
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)

Abstract

We study termination of LOTOS behaviors. In order to characterize termination, we first define a testing semantics for LOTOS in the classical way giving a fully abstract characterization in terms of acceptance sets. We show that this testing semantics does not properly capture termination. Then we modify the testing semantics by extending the class of admissible tests, to obtain a new equivalence that is a congruence with respect to the enabling operator. Then, we study alternative definitions of testing in order to capture termination, and we relate them each other, getting a Hierarchy of termination, which besides proves that the first termination semantics is in fact the most adequate one.

Keywords

Distributed Systems Process Algebras LOTOS Testing Semantics Termination. 

References

  1. Aceto, L. and Hennessy, M. (1992) Termination, deadlock, and divergence. Journal of the Association for Computer Machinery, 39 (1): 147–187.MathSciNetCrossRefzbMATHGoogle Scholar
  2. Bergstra, J. A. and Klop, J. W. (1984) Process algebra for syncronous communication. Information and Control, 60: 109–137.MathSciNetCrossRefzbMATHGoogle Scholar
  3. Brinksma, E., Scollo, G. and Steenhergen, E. (1986) LOTOS specifications, their implementations and their tests. In Proceedings of the Sixth Symposium on Protocol Specification, Testing and Verification, 349–360.Google Scholar
  4. de Nicola, R. and Hennessy, M. (1984) Testing equivalences for processes. Theoretical Computer Science, 34: 83–133.MathSciNetCrossRefzbMATHGoogle Scholar
  5. Hennessy, M. (1988) Algebraic Theory of Processes. MIT Press.zbMATHGoogle Scholar
  6. Hoare, C.A.R. (1985) Communicating Sequential Processes. Prentice Hall.zbMATHGoogle Scholar
  7. ISO (1988) LOTOS. A formal description technique based on the temporal ordering of observational behaviour. IS 8807, TC97/SC21.Google Scholar
  8. Milner, R. (1980) A Calculus of Communicating Systems. Lecture Notes in Computer Science 92. Springer-Verlag.Google Scholar
  9. Milner, R. (1989) Communication and Concurrency. Prentice Hall.zbMATHGoogle Scholar
  10. Quemada, J. (1994) Generalized termination and enabling. In Working Draft on Enhancements to LOTOS (Annex B). ISO/IEC JTC1/SC21/WG1.Google Scholar
  11. van Eijk, P., Diaz, M. and Vissers, C.A. editors (1989). The Formal Description Technique LOTOS. North-Holland.zbMATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • David de Frutos
    • 1
  • Manuel Múñez
    • 1
  • Juan Quemada
    • 2
  1. 1.1Dept. Informática y Automática, Facultad de CC. MatemáticasUniversidad Complutense de MadridMadridSpain
  2. 2.Dept. Ingeniería Telemática, E. T.S.I. TelecomunicaciónUniversidad Politécnica de MadridMadridSpain

Personalised recommendations