Verification of Quantitative Temporal Properties of SDL Specifications

Abstract. We describe an approach for the verification of quantitative temporal properties of SDL specifications, which adapts techniques developed for timed automata [2]. With respect to other verification approaches applied to SDL, our approach broadens the class of analyzable specifications and improves the handling of non-deterministic systems, such as open systems communicating with an unspecified environment. Compared to the initial framework of timed automata, the application of these verification techniques to SDL raises two interesting issues, discussed in the paper. They are: expressing the semantics of time in SDL in terms of timed automata concepts, and employing a user friendly automata-based property specification language (GOAL [1]) to express and verify temporal properties. The paper also presents a verification tool prototype for SDL which implements these ideas.

• Type: Conference
• Year: 2001
• Where: SDL
• Authors: Iulian Ober, Alain Kerbrat
• Keywords: Quantitative Temporal Properties, SDL 2001, SDL 2007, Temporal Properties, Timed Automata