A Formal Model for SDL Specifications Based on Timed Rewriting Logic

摘要

SDL is an industrial standard formal description technique for telecommunication systems. However, despite its wide spread use and industrial importance it lacks at present an adequate formal semantics integrating its static, dynamic, and real-time aspects. Timed Rewriting Logic (TRL) is a new timed variant of Rewriting Logic (RL), an algebraic formalism which allows the dynamic behaviour of systems to be axiomatised using rewrite rules. In this paper we define a new formal semantics for SDL using TRL which captures in a natural way the hierarchical structure, and the static and dynamic aspects of an SDL system. The semantics demonstrates the expressive power, versatility and automation advantages of using TRL. We consider how our new semantics can be used to simulate and reason about SDL specifications and in particular, we present an equivalence theorem that allows a wide range of TRL specifications to be implemented using RL and its associated tool support.