A Study on Verification of Service Specification in Communication Software Development

Kenji SHIBATA; Yoshihiro UEDA; Satsuki YUYAMA; Haruo HASEGAWA

A Study on Verification of Service Specification in Communication Software Development

Kenji SHIBATA, Yoshihiro UEDA, Satsuki YUYAMA, Haruo HASEGAWA

Full Text Views

0

Cite this

Summary :

This paper gives a verification method of a service specification in a communication system by utilizing Petri net. We define a service specification and clarify the feature of the specification. And we discuss a relation between a service specification and Petri net which represents the specification. Furthermore, this paper describes some kinds of verification for the specification and shows several examples. We are now developing a software support system-EXPRESS (EXPeRt system for ESS). EXPRESS designs automatically the service specification from user's requirements. In EXPRESS, each requirement is converted into ISG (Individual Service Graph) and all ISGs are integrated into TSG (Total Service Graph). TSG is the final service specification. ISG and TSG are described by using Petri net. Petri net is used for modeling a communication protocol and an asynchronous system. A service starts from an idle state and returns to the same idle state in a communication system. This means that a service specification should have a t-invariant. And a t-invariant which can not be decomposed is called a prime service. The followings are needed for verification of the specification: verification of ISG, detection of ISG from TSG and detection of other prime services than ISG. These are verified by utilizing an analysis of Petri net.

Publication: IEICE TRANSACTIONS on transactions Vol.E71-E No.12 pp.1203-1211

Publication Date: 1988/12/25

Publicized

Online ISSN

DOI

Type of Manuscript: Special Section PAPER (Special Issue on CAS Karuizawa Workshop)

Category

Authors

Kenji SHIBATA
Yoshihiro UEDA
Satsuki YUYAMA
Haruo HASEGAWA

Keyword

Cite this

Copy

Kenji SHIBATA, Yoshihiro UEDA, Satsuki YUYAMA, Haruo HASEGAWA, "A Study on Verification of Service Specification in Communication Software Development" in IEICE TRANSACTIONS on transactions, vol. E71-E, no. 12, pp. 1203-1211, December 1988, doi: .
Abstract: This paper gives a verification method of a service specification in a communication system by utilizing Petri net. We define a service specification and clarify the feature of the specification. And we discuss a relation between a service specification and Petri net which represents the specification. Furthermore, this paper describes some kinds of verification for the specification and shows several examples. We are now developing a software support system-EXPRESS (EXPeRt system for ESS). EXPRESS designs automatically the service specification from user's requirements. In EXPRESS, each requirement is converted into ISG (Individual Service Graph) and all ISGs are integrated into TSG (Total Service Graph). TSG is the final service specification. ISG and TSG are described by using Petri net. Petri net is used for modeling a communication protocol and an asynchronous system. A service starts from an idle state and returns to the same idle state in a communication system. This means that a service specification should have a t-invariant. And a t-invariant which can not be decomposed is called a prime service. The followings are needed for verification of the specification: verification of ISG, detection of ISG from TSG and detection of other prime services than ISG. These are verified by utilizing an analysis of Petri net.
URL: https://global.ieice.org/en_transactions/transactions/10.1587/e71-e_12_1203/_p

Copy

@ARTICLE{e71-e_12_1203,
author={Kenji SHIBATA, Yoshihiro UEDA, Satsuki YUYAMA, Haruo HASEGAWA, },
journal={IEICE TRANSACTIONS on transactions},
title={A Study on Verification of Service Specification in Communication Software Development},
year={1988},
volume={E71-E},
number={12},
pages={1203-1211},
abstract={This paper gives a verification method of a service specification in a communication system by utilizing Petri net. We define a service specification and clarify the feature of the specification. And we discuss a relation between a service specification and Petri net which represents the specification. Furthermore, this paper describes some kinds of verification for the specification and shows several examples. We are now developing a software support system-EXPRESS (EXPeRt system for ESS). EXPRESS designs automatically the service specification from user's requirements. In EXPRESS, each requirement is converted into ISG (Individual Service Graph) and all ISGs are integrated into TSG (Total Service Graph). TSG is the final service specification. ISG and TSG are described by using Petri net. Petri net is used for modeling a communication protocol and an asynchronous system. A service starts from an idle state and returns to the same idle state in a communication system. This means that a service specification should have a t-invariant. And a t-invariant which can not be decomposed is called a prime service. The followings are needed for verification of the specification: verification of ISG, detection of ISG from TSG and detection of other prime services than ISG. These are verified by utilizing an analysis of Petri net.},
keywords={},
doi={},
ISSN={},
month={December},}

Copy

TY - JOUR
TI - A Study on Verification of Service Specification in Communication Software Development
T2 - IEICE TRANSACTIONS on transactions
SP - 1203
EP - 1211
AU - Kenji SHIBATA
AU - Yoshihiro UEDA
AU - Satsuki YUYAMA
AU - Haruo HASEGAWA
PY - 1988
DO -
JO - IEICE TRANSACTIONS on transactions
SN -
VL - E71-E
IS - 12
JA - IEICE TRANSACTIONS on transactions
Y1 - December 1988
AB - This paper gives a verification method of a service specification in a communication system by utilizing Petri net. We define a service specification and clarify the feature of the specification. And we discuss a relation between a service specification and Petri net which represents the specification. Furthermore, this paper describes some kinds of verification for the specification and shows several examples. We are now developing a software support system-EXPRESS (EXPeRt system for ESS). EXPRESS designs automatically the service specification from user's requirements. In EXPRESS, each requirement is converted into ISG (Individual Service Graph) and all ISGs are integrated into TSG (Total Service Graph). TSG is the final service specification. ISG and TSG are described by using Petri net. Petri net is used for modeling a communication protocol and an asynchronous system. A service starts from an idle state and returns to the same idle state in a communication system. This means that a service specification should have a t-invariant. And a t-invariant which can not be decomposed is called a prime service. The followings are needed for verification of the specification: verification of ISG, detection of ISG from TSG and detection of other prime services than ISG. These are verified by utilizing an analysis of Petri net.
ER -