Characterizing Termination in LOTOS via Testing
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.
KeywordsDistributed Systems Process Algebras LOTOS Testing Semantics Termination.
- 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
- ISO (1988) LOTOS. A formal description technique based on the temporal ordering of observational behaviour. IS 8807, TC97/SC21.Google Scholar
- Milner, R. (1980) A Calculus of Communicating Systems. Lecture Notes in Computer Science 92. Springer-Verlag.Google Scholar
- Quemada, J. (1994) Generalized termination and enabling. In Working Draft on Enhancements to LOTOS (Annex B). ISO/IEC JTC1/SC21/WG1.Google Scholar