A verification support for communication software design

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