caa a22 4500 605516111 CHVBK 20210128100712.0 cr unu---uuuuu 210128e20150101xx s 000 0 eng 10.1007/s00165-014-0305-z doi (NATIONALLICENCE)springer-10.1007/s00165-014-0305-z Integrating stochastic reasoning into Event-B development [Elektronische Daten] [Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis] 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. British Computer Society, 2014 Event-B nationallicence Refinement nationallicence Probabilistic reasoning nationallicence Reliability nationallicence Responsiveness nationallicence Cyclic systems nationallicence Markov processes nationallicence Tarasyuk Anton Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland aut Troubitsyna Elena Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland aut Laibinis Linas Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland aut Formal Aspects of Computing Springer London 27/1(2015-01-01), 53-77 0934-5043 27:1<53 2015 27 165 https://doi.org/10.1007/s00165-014-0305-z text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0305-z text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Tarasyuk Anton Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland aut NATIONALLICENCE 700 1- Troubitsyna Elena Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland aut NATIONALLICENCE 700 1- Laibinis Linas Åbo Akademi University, Joukahaisenkatu 3-5, 20520, Turku, Finland aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/1(2015-01-01), 53-77 0934-5043 27:1<53 2015 27 165