Formal Automated Transformation of Lotos Specifications to SDL Specifications

摘要

In this paper, a formal method for automated transformation of a Lotos specification to an SDL specification is presented. The method is applicable to various Lotos specifications and to various communications protocols for various ISO OSI layers. This formal automated transformation facilitates immediate indirect applicability of future formal methods for derivation of testing sequences for SDL specifications to Lotos specifications. Firstly, the formal automated transformation method is applied to generate an SDL version. Then, the SDL-based derivation method is applied. This facilitates the best coverage of the testing sequences for Lotos specifications as the formal test derivation method with the best coverage can be applied. This also facilitates comparison of various test derivation methods in terms of coverage. It also facilitates alignment of ISO/IEC protocol/telecommunications protocols and TSS/ITU protocols.