Specification and Validation of Telephone Systems in LOTOS 1,2

LOTOS (Language of Temporal Ordering Specification) is a Formal Description Technique that was developed by the ISO for the specification of OSI services and protocols. In this paper we present a design methodology for the description in LOTOS of telephone systems with modern telephone features. The description of a Sample Telephone System is formalized. The LOTOS specification was extensively debugged and tested using the facilities provided by the University of Ottawa interpreter. 1