Introducing probabilistic reasoning within Event-B

Les méthodes de modélisation et de vérification formelles à base de preuves, par exemple le B événementiel, ne permettent pas, à ce jour, de bien prendre en compte l’ensemble des aspects quantitatifs des systèmes réels. En particulier, l’ajout d’aspects probabilistes dans les systèmes B événementiel est une problématique qui n’a pas été bien étudiée dans l’état de l’art. La difficulté réside principalement dans l’expression des probabilités ainsi que la vérification des aspects probabilistes dans ce formalisme. Dans cette thèse, une extension probabiliste au B événementiel est proposée pour permettre la description ainsi que la véri- fication des aspects probabilistes des systèmes. Nous désignons cette extension par le B événementiel probabiliste. Dans cette extension, nous proposons de remplacer toutes les sources de non-déterminisme en B événementiel par des probabilités, ce qui permettra ainsi la description des comportements purement probabilistes. Le processus de développement en B événementiel étant basé sur le raffinement, nous proposons plusieurs approches de développement basées sur le raffinement qui permettront l’intégration progressive des probabilités. En particulier, nous étudions la convergence presque certaine d’un ensemble d’événements dans cette extension. La méthode B événementiel est équipée de la plateforme Rodin que nous étendons pour permettre la prise en compte des éléments de l’extension. Les différents aspects de ce travail sont illustrés par plusieurs études de cas : un protocole de communication pair à pair, le système de train d’atterrissage d’un avion et un système de freinage d’urgence.From the best of our knowledge, proof based modeling and verification methods, for example Event-B, are not capable of handling the complete spectrum of quantitative aspects from real-life systems. In particular, modeling probabilistic aspects of systems within Event-B is a problem which has not been well studied in the state of the art. The main difficulties lie in the expression of probabilities and the verification of probabilistic aspects within Event-B. This thesis presents a probabilistic extension of Event-B to support modeling and verification of probabilistic aspects of systems. We denote this extension by probabilistic Event-B. We propose to replace all the non-deterministic choices by probabilistic choices, which allows the description of fully probabilistic systems. The development process in Event-B is based on refinement, we therefore propose some development approaches based on refinement which permit the progres- sive integration of probabilities in Event-B models. In particular, we study the almost-certain convergence of a set of events within this extension. The Event-B method is equipped with the Rodin platform which we extend to take into consideration the new added elements of our extension.The different aspects of this work are illustrated by several case studies: a peer-to-peer communication protocol, a landing gear sys- tem and an emergency brake system