Formal description of real-time systems using SDL

The Specification and Description Language (SDL) promises to be a good formal language to describe real-time systems, since it has time constructs and supports modeling of distributed systems. The problem with SDL is that it does not have a clear interpretation of time and does not provide a solid description of how the model is supposed to execute in time. This poses a problem for developing tools that can simulate and verify real-time systems described with SDL. In this paper, we present a technique to describe timing constraints in SDL along with our proposed semantic interpretation of these descriptions. We also present a method to understand how such an SDL description will run in time, and how simulation runs can be produced from the model. As an illustrative example, we use our description technique and interpretation of time to describe a railroad crossing in SDL, and we provide a time simulation run. Finally, we discuss the effect of this time semantics on the simulation and verification of SDL descriptions. We also discuss some missing functionalities regarding the temporal description of communication systems using SDL