Model checking SDL with Spin

D. Bosnacki, D.R. Dams, L. Holenderski, N. Sidorova

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

26 Citaten (Scopus)


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.
Originele taal-2Engels
TitelProceedings 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS2000) held as part of ETAPS2000, 25 March - 2 April 2000, Berlin, Germany
RedacteurenS. Graf, M.I. Schwartzbach
Plaats van productieBerlin
ISBN van geprinte versie3-540-67282-6
StatusGepubliceerd - 2000

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743

Vingerafdruk Duik in de onderzoeksthema's van 'Model checking SDL with Spin'. Samen vormen ze een unieke vingerafdruk.

Citeer dit