• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

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

Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis, Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B. In: John Derrick, Stefania Gnesi, Diego Latella, Helen Treharne (Eds.), Integrated Formal Methods - 9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012, Lecture Notes in Computer Science 7321, 237–252, Springer, 2012.

Abstract:

Modelling and refinement in Event-B provides a scalable sup- port for the development of complex service-oriented systems. Refinement in Event-B supports a systematic service development by a gradual trans- formation of an abstract specification into a detailed service architecture. In this paper we aim at integrating quantitative assessment of desired quality of essential service attributes into 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 represen- tation. By relying on probabilistic model-checking techniques, we allow for quantitative evaluation of quality of service attributes at early development stages. The approach is illustrated by a simple case study.

BibTeX entry:

@INPROCEEDINGS{inpTaTrLa12b,
  title = {Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B},
  booktitle = {Integrated Formal Methods - 9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012},
  author = {Tarasyuk, Anton and Troubitsyna, Elena and Laibinis, Linas},
  volume = {7321},
  series = {Lecture Notes in Computer Science},
  editor = {Derrick, John and Gnesi, Stefania and Latella, Diego and Treharne, Helen},
  publisher = {Springer},
  pages = {237–252},
  year = {2012},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 1

Edit publication