Computer-aided design tools for Markovian analysis and verification of digital circuits have gained much interest in the last few years. This is mainly due to the advent of effective data structures, e.g., binary and algebraic decision diagrams, for Boolean and pseudo-Boolean function representation and manipulation. The authors illustrate how those tools can be successfully exploited to analyze the behavior and verify the correctness of a communication protocol. They first consider the case of single protocol entities running in isolation, and present a simple application example (i.e. the sender entity of the alternating bit protocol). Then, informally illustrate how the analysis approach can be extended to the general case of multi-layer protocol stacks and complete communication systems.

Application of symbolic FSM Markovian analysis to protocol verification / Baldi, Mario; Macii, Alberto; Macii, Enrico; Poncino, Massimo. - In: IEE PROCEEDINGS. COMPUTERS AND DIGITAL TECHNIQUES. - ISSN 1350-2387. - 146:5(1999), pp. 221-226. [10.1049/ip-cdt:19990645]

Application of symbolic FSM Markovian analysis to protocol verification

BALDI, MARIO;MACII, Alberto;MACII, Enrico;PONCINO, MASSIMO
1999

Abstract

Computer-aided design tools for Markovian analysis and verification of digital circuits have gained much interest in the last few years. This is mainly due to the advent of effective data structures, e.g., binary and algebraic decision diagrams, for Boolean and pseudo-Boolean function representation and manipulation. The authors illustrate how those tools can be successfully exploited to analyze the behavior and verify the correctness of a communication protocol. They first consider the case of single protocol entities running in isolation, and present a simple application example (i.e. the sender entity of the alternating bit protocol). Then, informally illustrate how the analysis approach can be extended to the general case of multi-layer protocol stacks and complete communication systems.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/1402029
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo