In the design process of communication software, its specificationnneeds to be rigorously defined without leaving any ambiguity. For thisnpurpose, several FDTs (formal description techniques) have been proposednfor the description of a rigorous specification. We developed a supportnenvironment for highly reliable computer aided software design based onnFDTs. The paper proposes an integrated support environment, named ITECS,nwhich has been developed based on LOTOS as the FDTs, to support a formalndescription of communication software specification and verification.nITECS comprises of two subsystems: one to support specification of thenmessage sequence charts and graphical LOTOS specifications, and thenother to support the verification of LOTOS specifications. This paperndiscusses the specification support of the ITECS environment
展开▼
