Skip to topic | Skip to bottom


Main.YvesBourgoisr1.1 - 08 Oct 2007 - 12:07 - GerdGross

Start of topic | Skip to actions

-- GerdGross - 08 Oct 2007

Yves Bourgeois

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.

You are here: Main > MastersProjects > PastAndCurrentMScProjects > YvesBourgois

to top

Copyright © 2003-2017, Software Engineering Research Group, Delft University of Technology, The Netherlands