Automated enrichment of SDL specifications with MSCs

Formal methods and Formal Description Techniques (FDT) are becoming more and more important for developing complex real-time and distributed systems. Message Sequence Charts (MSC) and Specification and Description Language (SDL) are standardized FDTs for specification of telecommunication protocols in particular and distributed systems in general. We present an automated approach for enriching an SDL specification with MSC. This approach can be used for incremental development with SDL and MSC or for maintenance of a system in SDL. Enrichment of SDL with MSC involves enrichment of SDL architecture and behavior. Our automated approach consists of three interconnected steps i.e. pre-phase, MSC2SDL phase and post-phase . In the pre-phase SDL architecture is enriched using new MSC. We give algorithms for enriching SDL architecture using MSC. MSC2SDL phase generates new SDL behavior using new MSC and enriched architecture. This phase uses MSC2SDL tool. Finally, the post-phase merges old and new SDL behavior to get enriched SDL. We have developed 14 rules of behavioral merger based upon a formal extension relation which guarantees to preserve all the old behavior and prevents introduction of new non-determinism in the enriched specifications. Furthermore, we have developed tools for pre-phase and post-phase and they have been connected with MSC2SDL tool to get a tool set for automated enrichment