THESE-bertrand06

N. Bertrand. Modèles stochastiques pour les pertes de messages dans les protocoles asynchrones et techniques de vérification automatique. PhD Thesis Laboratoire Spécification et Vérification, ENS Cachan, France, September 2006.

Download [help]

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

Asynchronous communication protocols are naturally seen as communicating finite automata over unbounded FIFO channels. In this thesis, we consider variants of LCS (Lossy Channel Systems) for which message losses are probabilistic. More precisely, we introduce the models of Probabilistic LCS (PLCS), and Nondeterministic and Probabilistic LCS (NPLCS) whose semantics are respectively Markov chains and Markov decision processes. A general criterion on convergence of fixed points expressions in Well Structured Transition Systems allows to prove a number a decidability results with respect to verification of linear-time properties for both models. We also prove undecidability results to show the limits of these models. A prototype tool in OCaml implements the algorithms of this thesis. Despite the high complexity of the problems, this tool allows to prove liveness properties of commmunication protocols such as the Alternating Bit Protocol and Pachl's protocol

Contact

Nathalie Bertrand http://www.irisa.fr/prive/nbertran/

BibTex Reference

@PhdThesis{THESE-bertrand06,
   Author = {Bertrand, N.},
   Title = {Mod{è}les stochastiques pour les pertes de messages dans les protocoles asynchrones et techniques de v{é}rification automatique},
   School = {Laboratoire Sp{é}cification et V{é}rification, ENS Cachan, France},
   Month = {September},
   Year = {2006}
}

EndNote Reference [help]

Get EndNote Reference (.ref)