Abstract
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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abrial J-R (1996) Extending B without changing it (for developing distributed systems). In: Habiras H (ed) First Conference on the B method, pp 169–190
Abrial J-R (2005) The B-Book: assigning programs to meanings. Cambridge University Press, Cambridge
Abrial J-R (2010) Modeling in Event-B. Cambridge University Press, Cambridge
Avizienis A., Laprie J-C., Randell B., Landwehr CE (2004) Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secur Comput 1(1): 11–33
Bresciani R, Butterfield A (2012) A UTP semantics of pGCL as a homogenous relation. In: IFM 2012. Springer, Belin, pp 191–205
Butler M, Falampin J (2002) An approach to modelling and refining timing properties in B. In: Refinement of critical systems (RCS)
Back RJR., von Wright J (1998) Refinement calculus: a systematic introduction. Springer, Berlin
Mani Chandy K., Misra J (1988) Parallel program design: a foundation. Addison-Wesley, USA
Chu WW, Sit C-M (1988) Estimating task response time with contentions for real-time distributed systems. In: Real-Time Systems Symposium. IEEE Computer Society, pp 272–281
DEPLOY (2008) Industrial deployment of system engineering methods providing high dependability and productivity. IST FP7 IP Project. Online at http://www.deploy-project.eu/
Event-B and Rodin Documentation Wiki.Qualitative probability plug-in. Online at http://wiki.event-b.org/index.php/Event-B_Qualitative_Probability_User_Guid.
Hansson H (1995) Time and probability in formal design of distributed systems. Elsevier, London
Hallerstede S, Hoang TS (2007) Qualitative probabilistic modelling in Event-B. In: Davies J, Gibbons J (eds) IFM 2007, Integrated Formal Methods. Springer, Berlin, pp 293–312
He J, Sanders JW (2006) Unifying probability. In: Proceedings of First International Symposium on Unifying Theories of Programming, UTP 2006. Springer, New York, pp 173–199
Hinderer K, Waldmann T-H (2003) The critical discount factor for finite Markovian decision processes with an absorbing set. In: Mathematical methods fo operations research. Springer, Berlin, pp 1–19
Iliasov A (2011) Use case scenarios as verification conditions: Event-B/Flow approach. In: SERENE 2011, Software Engineering for Resilient Systems. Springer, Berlin, pp 9–23
Iliasov A, Laibinis L, Troubitsyna E, Romanovsky A, Latvala T (2012) Augmenting Event-B modelling with real-time verification. In: FormSERA 2012, Formal Methods in Software Engineering: Rigorous and Agile Approaches. IEEE Press, New York, pp 51–57
Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: CAV’11, International Conference on Computer Aided Verification. Springer, Berlin, pp 585–591
Kemeny JG, Snell JL (1960) Finite Markov chains. D. Van Nostrand Company, Princeton, NJ
Larsen KG, Skou A (1991) Bisimulation through probabilistic testing. In: Information and Computation 94, pp 1–28
McIver AK., Morgan CC (2005) Abstraction, refinement and proof for probabilistic systems. Springer, New York
McIver AK, Morgan CC, Troubitsyna E (1998) The probabilistic steam boiler: a case study in probabilistic data refinement. In: International Refinement Workshop, ANU, Canberra. Springer, Berlin
Meinicke L, Solin K (2010) Refinement algebra for probabilistic programs. Form Asp Comput 22: 3–31
O’Connor PDT (1995) Practical reliability engineering. 3rd edn. Wiley, Toronto
Puterman M (2005) Markov decision processes. Discrete stochastic dynamic programming, Wiley Toronto
Rao JR (1995) Extension of the UNITY methodology: compositionality, fairness and probability in parallelism. Springer, Berlin
Rodin Platform. Integrated Development Environment for Event-B. Online at http://www.event-b.org/
RODIN: Rigorous Open Development Environment for Complex Systems. (2004) IST FP6 STREP project. Online at http://rodin.cs.ncl.ac.uk/
Segala R., Lynch N. (1995) Probabilistic simulations for probabilistic processes. Nord J Comput 2(2): 250–273
Sere K, Troubitsyna E (1996) Probabilities in action systems. In: Nordic Workshop on Programming Theory
Schneider S, Treharne H, Wehrheim H (2010) A CSP approach to control in Event-B. In: IFM 2010. Springer, Berlin, pp 260–274
Stoddart B., Zeyda F. (2013) A unification of probabilistic choice within a design-based model of reversible computation. Form Asp Comput 25: 107–131
Tarasyuk A, Pereverzeva I, Troubitsyna E, Latvala T, Nummila L (2012) Formal development and assessment of a reconfigurable on-board satellite system. In: SAFECOMP 2012. Springer, Berlin, pp 210–222
Tarasyuk A, Pereverzeva I, Troubitsyna E, Laibinis L (2013) Formal development and quantitative assessment of a resilient multi-robotic system. In: SERENE 2013. Springer, Berlin, pp 109–124
Trivedi K., Ramani S., Fricks R (2003) Recent advances in modeling response-time distributions in real-time systems. In: Proceedings of the IEEE 91(7): 1023–1037
Troubitsyna E. (1999) Reliability assessment through probabilistic refinement. Nord J Comput 6(3): 320–342
Tarasyuk A, Troubitsyna E, Laibinis L (2010) From formal specification in Event-B to probabilistic reliability assessment. In: DEPEND 2010. IEEE Computer Society, Los Alamitos, CA, pp 24–31
Tarasyuk A, Troubitsyna E, Laibinis L (2010) Towards probabilistic modelling in Event-B. In: IFM 2010, Integrated Formal Methods. Springer, Berlin, pp 275–289
Tarasyuk A, Troubitsyna E, Laibinis L (2012) Formal modelling and verification of service-oriented systems in probabilistic Event-B. In: IFM 2012, Integrated Formal Methods. Springer, Berlin, pp 237–252
Villemeur A (1995) Reliability, availability, maintainability and safety assessment. Wiley, New York
White DJ (1993) Markov decision processes. Wiley, New York
Yilmaz E, Hoang TS (2010) Development of Rabin’s choice coordination algorithm in Event-B. ECEASST, 35
Author information
Authors and Affiliations
Corresponding author
Additional information
Michael J. Butler
Rights and permissions
About this article
Cite this article
Tarasyuk, A., Troubitsyna, E. & Laibinis, L. Integrating stochastic reasoning into Event-B development. Form Asp Comp 27, 53–77 (2015). https://doi.org/10.1007/s00165-014-0305-z
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-014-0305-z