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.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copy
Keiichirou YAMANO, Dusan JOKANOVIC, Tsuyoshi ANDO, Masataka OHTA, Kaoru TAKAHASHI, "Formal Specification and Verification of ISDN Services in LOTOS" in IEICE TRANSACTIONS on Communications,
vol. E75-B, no. 8, pp. 715-722, August 1992, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/communications/10.1587/e75-b_8_715/_p
Copy
@ARTICLE{e75-b_8_715,
author={Keiichirou YAMANO, Dusan JOKANOVIC, Tsuyoshi ANDO, Masataka OHTA, Kaoru TAKAHASHI, },
journal={IEICE TRANSACTIONS on Communications},
title={Formal Specification and Verification of ISDN Services in LOTOS},
year={1992},
volume={E75-B},
number={8},
pages={715-722},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={August},}
Copy
TY - JOUR
TI - Formal Specification and Verification of ISDN Services in LOTOS
T2 - IEICE TRANSACTIONS on Communications
SP - 715
EP - 722
AU - Keiichirou YAMANO
AU - Dusan JOKANOVIC
AU - Tsuyoshi ANDO
AU - Masataka OHTA
AU - Kaoru TAKAHASHI
PY - 1992
DO -
JO - IEICE TRANSACTIONS on Communications
SN -
VL - E75-B
IS - 8
JA - IEICE TRANSACTIONS on Communications
Y1 - August 1992
AB - 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.
ER -