Application of symbolic FSM Markovian analysis to protocol verification

Computer-aided design tools for Markovian analysis and verification of digi tal circuits have gained much interest in the last few years. This is mainl y due to the advent of effective data structures, e.g., binary and algebrai c decision diagrams, for Boolean and pseudo-Boolean function representation and manipulation. The authors illustrate how those tools can be successful ly exploited to analyse the behavior and verify the correctness of a commun ication protocol. They first consider the case of single protocol entities running in isolation, and present a simple application example (i.e. the se nder entity of the alternating bit protocol). Then, informally illustrate h ow the analysis approach can be extended to the general case of multi-layer protocol stacks and complete communication systems.