Formal Specification and Verification of ISDN Services in LOTOS

Keiichirou YAMANO  Dusan JOKANOVIC  Tsuyoshi ANDO  Masataka OHTA  Kaoru TAKAHASHI  

IEICE TRANSACTIONS on Communications   Vol.E75-B    No.8    pp.715-722
Publication Date: 1992/08/25
Online ISSN: 
Print ISSN: 0916-8516
Type of Manuscript: Special Section PAPER (Special Issue on the 4th Japan-Korea Joint Conference on Communications, Networks, Switching Systems and Satellite Communications (4th JC-CNSS))
LOTOS,  specification,  verification,  switching software,  

Full Text: PDF(659.5KB)>>
Buy this Article

In this paper an approach to formal specification and verification of ISDN services in LOTOS is presented. As for specification, it is shown that LOTOS can be effectively applied to describe different levels of ISDN service specifications. At the higher level, only the external behaviour of the network is specified. On the other hand, at the lower level, specifications include the behaviour of network components such as switching systems, where each switching system can be specified independently of each other. Such specification style, proves suitable for verification of specifications by using the concepts of the simulation relation.