Title :
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
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;
Conference_Titel :
Software Engineering Conference, 2000. APSEC 2000. Proceedings. Seventh Asia-Pacific
Print_ISBN :
0-7695-0915-0
DOI :
10.1109/APSEC.2000.896686
