Verification of a wireless ATM medium-access protocol

Author

Sidorova, Natalia ; Steffen, Martin

Author_Institution

Dept. of Math. & Comput. Sci., Eindhoven Univ. of Technol., Netherlands

fYear

2000

fDate

2000

Firstpage

84

Lastpage

91

Abstract

We report on a model checking case study of an industrial medium access protocol for wireless ATM. Since the protocol is too large to be verified by any of the existing checkers as a whole, the verification exploits the layered and modular structure of the protocol´s SDL specification and proceeds in a bottom-up, compositional way. The compositional arguments are used in combination with abstraction techniques to further reduce the state space of the system. The verification is primarily aimed at debugging the system. After correcting the specification step by step and validating various untimed and time-dependent properties, a model of the whole control component of the medium-access protocol is built and verified. The significance of the case study is in demonstrating that verification tools can handle complex properties of a model as large as shown

Keywords

access protocols; asynchronous transfer mode; formal specification; formal verification; wireless LAN; SDL specification; abstraction techniques; medium-access protocol verification; model checking; modular structure; state space reduction; system debugging; time-dependent properties; untimed properties; wireless ATM; Access protocols; Automatic logic units; Computer science; Context modeling; Debugging; Electrical equipment industry; Error correction; Mathematics; State-space methods; Wireless application protocol;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering Conference, 2000. APSEC 2000. Proceedings. Seventh Asia-Pacific

ISSN

1530-1362

Print_ISBN

0-7695-0915-0

Type

conf

DOI

10.1109/APSEC.2000.896686

Filename

896686