Reliability in Fully Probabilistic Event-B: How to Bound the Enabling of Events
| Autor: | Arnaud Lanoix, Syrine Aouadi |
|---|---|
| Přispěvatelé: | Architectures et Logiciels Sûrs (AeLoS), Laboratoire des Sciences du Numérique de Nantes (LS2N), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT) |
| Rok vydání: | 2018 |
| Předmět: |
Theoretical computer science
Probabilistic Event-B Computer science Reliability (computer networking) Probabilistic logic [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] 0102 computer and information sciences 02 engineering and technology Reliability Weight 16. Peace & justice 01 natural sciences Upper and lower bounds Set (abstract data type) Constraint (information theory) 010201 computation theory & mathematics Bounding overwatch Probabilistic properties 0202 electrical engineering electronic engineering information engineering Event-B 020201 artificial intelligence & image processing Limit (mathematics) Proof obligations Event (probability theory) |
| Zdroj: | Communications in Computer and Information Science ISBN: 9783030028510 MEDI Workshops New Trends in Model and Data Engineering MEDI 2018 International Workshops, DETECT, MEDI4SG, IWCFS, REMEDY, Marrakesh, Morocco, October 24–26, 2018, Proceedings New Trends in Model and Data Engineering-MEDI 2018 Workshops: DETECT, MEDI4SG, IWCFS, REMEDY New Trends in Model and Data Engineering-MEDI 2018 Workshops: DETECT, MEDI4SG, IWCFS, REMEDY, Oct 2018, Marrakesh, Morocco. https://www.springer.com/gp/book/9783030028510 |
| DOI: | 10.1007/978-3-030-02852-7_17 |
| Popis: | International audience; In previous work, we have proposed a fully probabilistic version of Event-B where all the non-deterministic choices are replaced by probabilistic ones and, particularly, the events are equipped with weights that allow us to consider their enabling probability. In this work, we focus on the reliability of the system by proposing to constraint the probability of enabling an event (or a set of events) to control its importance with regard to the intended system behaviour. We add a specific upper bound which must limit the enabling probabilities of the chosen events and we consider the necessary proof obligations to check that the considered events respect the bound. At the end, we illustrate our work by presenting a case study specified in probabilistic Event-B and where bounding the enabling of some events is mandatory. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|