Name
Abstract | ||
|---|---|---|
We present an attempt to use the model checker Spin as a verification engine for SDL, with special emphasis put on the verification of timing properties of SDL models. We have extended Spin with a front-end that allows to translate SDL to Promela (the input language of Spin), and a back-end that allows to analyse timing properties. Compared with the previous attempts, our approach allows to verify not only qualitative but also quantitative aspects of SDL timers, and our translation of SDL to Promela handles the SDL timers in a correct way. We applied the toolset to the verification of a substantial part of a complex industrial protocol. This allowed to expose several non-trivial errors in the protocol's design. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1007/3-540-46419-0_25 | TACAS |
Keywords | Field | DocType |
extended spin,non-trivial error,model checking sdl,sdl model,timing property,input language,complex industrial protocol,verification engine,previous attempt,sdl timers,model checker spin,model checking,front end | Spin-½,Programming language,Model checking,Computer science,Formal specification,Real-time operating system,Theoretical computer science,Promela,Partial order reduction,Software development,Embedded system,Formal verification | Conference |
Volume | ISSN | ISBN |
1785 | 0302-9743 | 3-540-67282-6 |
Citations | PageRank | References |
18 | 1.11 | 7 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dragan Bosnacki | 1 | 276 | 26.95 |
| dennis dams | 2 | 137 | 7.90 |
| Leszek Holenderski | 3 | 154 | 16.67 |
| Natalia Sidorova | 4 | 657 | 54.08 |