- 08 Oct 2007
Design and Verification of Concurrent Real-Time Systems using SDL and MSC
This thesis examines both the shortcomings of the Formal Description Languages SDL and MSC, when they are used to design hard real-time systems, and the lack of verification tools to verify the timing requirements of such hard real-time systems. In the first part of this document we will discuss that SDL and MSC do not have a proper model of time, or a formal way to express all aspects of real-time systems. Therefore, we propose a set of semantic rules, which make it possible to formally describe these timing requirements. In the second part, we will discuss how we can statically verify the temporal properties of the SDL and MSC model, using the UPPAAL verification tool, together with a case study that proves the correctness of the proposed method.