Verifying large SDL-specifications using model checking

N. Sidorova, M. Steffen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

10 Citations (Scopus)
1 Downloads (Pure)

Abstract

In this paper we propose a methodology for model-checking based verification of large SDL specifications. The methodology is illustrated by a case study of an industrial medium-access protocol for wireless ATM. To cope with the state space explosion, the verification exploits the layered and modular structure of the protocol’s SDL specification and proceeds in a bottom-up compositional way. To make a compositional approach feasible in practice, we develop a technique for losing SDL components with a chaotic environment without incurring the state-space penalty of considering all possible combinations of values in the input queues. The compositional arguments are used in combination with abstraction techniques to further reduce the state space of the system. With debugging the system as the prime goal of the verification, we corrected the specification step by step and validated various untimed and time-dependent properties until we built and verified a model of the whole control component of the medium-access protocol. The significance of the case study is in demonstrating that verification tools can handle complex properties of a model as large as shown.
Original languageEnglish
Title of host publicationSDL 2001: Meeting UML (Proceedings 10th International SDL Forum, Copenhagen, Denmark, June 27-29, 2001)
EditorsR. Reed, J. Reed
Place of PublicationBerlin
PublisherSpringer
Pages403-420
ISBN (Print)3-540-42281-1
DOIs
Publication statusPublished - 2001

Publication series

NameLecture Notes in Computer Science
Volume2078
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Verifying large SDL-specifications using model checking'. Together they form a unique fingerprint.

Cite this