Integrating stochastic reasoning into Event-B development
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605516111 | ||
| 003 | CHVBK | ||
| 005 | 20210128100712.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150101xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-014-0305-z |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-014-0305-z | ||
| 245 | 0 | 0 | |a Integrating stochastic reasoning into Event-B development |h [Elektronische Daten] |c [Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis] |
| 520 | 3 | |a Dependability is a property of a computer system to deliver services that can be justifiably trusted. Formal modelling and verification techniques are widely used for development of dependable computer-based systems to gain confidence in the correctness of system design. Such techniques include Event-B—a state-based formalism that enables development of systems correct-by-construction. While Event-B offers a scalable approach to ensuring functional correctness of a system, it leaves aside modelling of non-functional critical properties, e.g., reliability and responsiveness, that are essential for ensuring dependability of critical systems. Both reliability, i.e., the probability of the system to function correctly over a given period of time, and responsiveness, i.e., the probability of the system to complete execution of a requested service within a given time bound, are defined as quantitative stochastic measures. In this paper, we propose an extension of the Event-B semantics to enable stochastic reasoning about dependability-related non-functional properties of cyclic systems. We define the requirements that a cyclic system should satisfy and introduce the notions of reliability and responsiveness refinement. Such an extension integrates reasoning about functional correctness and stochastic modelling of non-functional characteristics into the formal system development. It allows the designer to ensure that a developed system does not only correctly implement its functional requirements but also satisfies given non-functional quantitative constraints. | |
| 540 | |a British Computer Society, 2014 | ||
| 690 | 7 | |a Event-B |2 nationallicence | |
| 690 | 7 | |a Refinement |2 nationallicence | |
| 690 | 7 | |a Probabilistic reasoning |2 nationallicence | |
| 690 | 7 | |a Reliability |2 nationallicence | |
| 690 | 7 | |a Responsiveness |2 nationallicence | |
| 690 | 7 | |a Cyclic systems |2 nationallicence | |
| 690 | 7 | |a Markov processes |2 nationallicence | |
| 700 | 1 | |a Tarasyuk |D Anton |u Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland |4 aut | |
| 700 | 1 | |a Troubitsyna |D Elena |u Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland |4 aut | |
| 700 | 1 | |a Laibinis |D Linas |u Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/1(2015-01-01), 53-77 |x 0934-5043 |q 27:1<53 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-014-0305-z |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-014-0305-z |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Tarasyuk |D Anton |u Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Troubitsyna |D Elena |u Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Laibinis |D Linas |u Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/1(2015-01-01), 53-77 |x 0934-5043 |q 27:1<53 |1 2015 |2 27 |o 165 | ||