Sciweavers

Share
SDL
2001

Verification of Quantitative Temporal Properties of SDL Specifications

10 years 1 months ago
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.
Iulian Ober, Alain Kerbrat
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2001
Where SDL
Authors Iulian Ober, Alain Kerbrat
Comments (0)
books