Title :
A verification support for communication software design
Author :
Yamano, Keiichiro ; Tokita, Yoshiaki ; Takahashi, Kaoru
Author_Institution :
AIC System Labs., Sendai, Japan
Abstract :
In communication software design, it is important to describe the specification without any errors or ambiguity. For this purpose, several formal description techniques have been proposed to ensure rigorous specifications. In addition, it is necessary to facilitate the generation of highly reliable specification. We propose an integrated support environment, named ITECS (integrated environment for high reliability communication software design), which has been developed to support the design of highly reliable communication software efficiently. ITECS has the following characteristics: it is based on the formal description technique LOTOS, to describe the specification rigorously; it has specification functions to support editing of message sequence charts and graphical LOTOS specifications; it has verification functions based on the mathematical basis of LOTOS. This paper mainly discusses ITECS´s verification of consistency between two LOTOS specifications in the refinement process of specification design
Keywords :
CAD; formal specification; formal verification; software reliability; telecommunication computing; ITECS; LOTOS; communication software design; consistency; formal description techniques; graphical LOTOS specifications; integrated environment for high reliability communication software design; integrated support environment; message sequence charts; refinement process; specification; specification design; specification functions; verification functions; verification support; Communication standards; Computer errors; Educational institutions; LAN interconnection; Laboratories; Natural languages; Open systems; Process design; Software design; Software standards;
Conference_Titel :
Global Telecommunications Conference, 1995. GLOBECOM '95., IEEE
Print_ISBN :
0-7803-2509-5
DOI :
10.1109/GLOCOM.1995.500288
