Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B

  • Anton Tarasyuk
  • Elena Troubitsyna
  • Linas Laibinis
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7321)


Modelling and refinement in Event-B provides a scalable support for systematic development of complex service-oriented systems. This is achieved by a gradual transformation of an abstract service specification into its detailed architecture. In this paper we aim at integrating quantitative assessment of essential quality of service attributes into the formal modelling process. We propose an approach to creating and verifying a dynamic service architecture in Event-B. Such an architecture can be augmented with stochastic information and transformed into the corresponding continuous-time Markov chain representation. By relying on probabilistic model-checking techniques, we allow for quantitative evaluation of quality of service at early development stages.


Service Director Service Request Parallel Composition Service Execution Abstract State Machine 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (2005)Google Scholar
  2. 2.
    Abrial, J.R.: Modeling in Event-B. Cambridge University Press (2010)Google Scholar
  3. 3.
    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying Continuous Time Markov Chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  4. 4.
    Baier, C., Katoen, J.-P., Hermanns, H.: Approximate Symbolic Model Checking of Continuous-Time Markov Chains (Extended Abstract). In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 146–161. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  5. 5.
    Calinescu, R., Grunske, L., Kwiatkowska, M., Mirandola, R., Tamburrelli, G.: Dynamic QoS Management and Optimization in Service-Based Systems. IEEE Trans. Softw. Eng. 37, 387–409 (2011)CrossRefGoogle Scholar
  6. 6.
    De Nicola, R., Latella, D., Loreti, M., Massink, M.: MarCaSPiS: a Markovian Extension of a Calculus for Services. Electronic Notes in Theoretical Computer Science 229(4), 11–26 (2009)CrossRefGoogle Scholar
  7. 7.
    Grunske, L.: Specification patterns for probabilistic quality properties. In: International Conference on Software Engineering, ICSE 2008, pp. 31–40. ACM (2008)Google Scholar
  8. 8.
    Iliasov, A.: Use Case Scenarios as Verification Conditions: Event-B/Flow Approach. In: Troubitsyna, E.A. (ed.) SERENE 2011. LNCS, vol. 6968, pp. 9–23. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    Industrial Deployment of System Engineering Methods Providing High Dependability and Productivity (DEPLOY): IST FP7 IP Project,
  10. 10.
    Kitchin, D., Quark, A., Cook, W., Misra, J.: The Orc Programming Language. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS/FORTE 2009. LNCS, vol. 5522, pp. 1–25. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  11. 11.
    Laibinis, L., Troubitsyna, E., Leppänen, S.: Formal Reasoning about Fault Tolerance and Parallelism in Communicating Systems. In: Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.) Methods, Models and Tools for Fault Tolerance. LNCS, vol. 5454, pp. 130–151. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  12. 12.
    Laibinis, L., Troubitsyna, E., Leppänen, S., Lilius, J., Malik, Q.A.: Formal Model-Driven Development of Communicating Systems. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 188–203. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Lapadula, A., Pugliese, R., Tiezzi, F.: A Calculus for Orchestration of Web Services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 33–47. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. 14.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  15. 15.
    McIver, A.K., Morgan, C.C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2005)Google Scholar
  16. 16.
    Prandi, D., Quaglia, P.: Stochastic COWS. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 245–256. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Rodin: Event-B Platform,
  18. 18.
    Schneider, S., Treharne, H., Wehrheim, H.: A CSP Approach to Control in Event-B. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 260–274. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  19. 19.
    Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Quantitative Reasoning about Dependability in Event-B: Probabilistic Model Checking Approach. In: Dependability and Computer Engineering: Concepts for Software-Intensive Systems, pp. 459–472. IGI Global (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Anton Tarasyuk
    • 1
    • 2
  • Elena Troubitsyna
    • 2
  • Linas Laibinis
    • 2
  1. 1.Turku Centre for Computer ScienceTurkuFinland
  2. 2.Åbo Akademi UniversityTurkuFinland

Personalised recommendations