In the design process of communication software, its specification needs to be rigorously defined without leaving any ambiguity. For this purpose, several FDTs (formal description techniques) have been proposed for the description of a rigorous specification. We developed a support environment for highly reliable computer aided software design based on FDTs. The paper proposes an integrated support environment, named ITECS, which has been developed based on LOTOS as the FDTs, to support a formal description of communication software specification and verification. ITECS comprises of two subsystems: one to support specification of the message sequence charts and graphical LOTOS specifications, and the other to support the verification of LOTOS specifications. This paper discusses the specification support of the ITECS environment.
展开▼
