Design, specification, and validation of telephony systems in LOTOS.

Abstract

LOTOS (Language Of Temporal Ordering Specification) is a Formal Description Technique (FDT) based on the temporal ordering of observational behaviour. It was developed by ISO (International Organization for Standardization) for the specification of OSI (Open Systems Interconnection) services and protocols. The topic of this thesis is first to present a Sample Telephone System, then formalize it using the FDT language LOTOS. The resulting LOTOS specification is then validated using an interpreter. Testing the design of the specification is also discussed. The thesis is structured as follows: in Chapter 1, we present an introduction to formal description techniques along with a review of some relevant existing work and the objective of this thesis. The next Chapter gives an overview of the LOTOS language. In Chapter 3, we discuss concepts of design of telecommunication systems. The Chapter includes an overview of telecommunication systems along with an informal description of a Sample Telephone System. In Chapter 4, we discuss the formal description in LOTOS of the Sample Telephone System presented in Chapter 3. Validation and testing of the specification are also part of Chapter 3. The conclusions of the thesis along with a discussion of possible future work follow in Chapter 5. Appendix A presents some technical abbreviations, and the Sample Telephone Specification is presented in Appendix B. In Appendix C, we present a set of test processes used to test the Sample Telephone Specification. Finally, some important symbolic trees of processes are presented in Appendix D.