Practical Applications of Probabilistic Model Checking to Communication Protocols
Marie Duflot, Marta Kwiatkowska, Gethin Norman, David A. Parker, Sylvain Peyronnet, Claudine Picaronny, Jeremy Sproston · Formal Methods for Industrial Critical Systems · 2012
This chapter describes work that has been carried out to apply formal verification techniques to communication protocols. It gives an overview of probabilistic timed automata (PTA), probabilistic model checking, and the corresponding implementation techniques and tools. This chapter illustrates their usefulness in the domain of communication protocols through a case study: the IEEE 802.3 (Carrier Sense Multiple Access/ Collision Detection [CSMA/CD]) protocol, as used for example in networking over Ethernet. Probabilistic model checking is a formal verification technique for the modeling and analysis of systems that exhibit stochastic behavior. The chapter presents an illustrative case study of a randomized communication protocol, analyzed using PTA and probabilistic model checking. It uses the CSMA/CD protocol, which is a fundamental part of the IEEE 802.3 international standard (Ethernet Network Communication protocol). Controlled Vocabulary Terms carrier sense multiple access; protocols