PhD Defense
Nathalie Bertrand
Title of the thesis
Stochastic models for Lossy Channel Systems, and automated
verification techniques.
Day and Location
Friday October 6th in Cachan at 2pm.
Salle de conférences, Pavillon des Jardins, École Normale Supérieure
de Cachan.
Access
Jury
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 of decidability results wrt
verification of linera 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
complexity of the problems, this tool allows to prove liveness
properties of communication protocols such as the Alternating Bit
Protocol and Pachl's protocol.
Keywords
Formal verification, Lossy Channel Systems, Probabilities.