A Verification Scheme for Service Specifications Described by Information Sequence Charts

Mitsuhiro OKAMOTO  Yoshihiro NIITSU  

IEICE TRANSACTIONS on Communications   Vol.E75-B   No.10   pp.978-985
Publication Date: 1992/10/25
Online ISSN: 
Print ISSN: 0916-8516
Type of Manuscript: Special Section PAPER (Special Issue on Communication Software Technologies)
specification description,  specification verification,  

Full Text: PDF>>
Buy this Article

This paper describes a verification scheme for service specifications and presents verification results for prototype system. Verified specifications are described by information sequence charts, which describe the communicating states between users and the messages between a user and a network. The verification scheme consists of two steps: macro sequence verification, which treats rough transitions of states, and transition procedure verification, which treats procedure of all messages. A prototype verification system demonstrates that this scheme can detect about 90% of errors in a specification within 4.4 seconds.