Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Formal Derivation of a Distrib...

Formal Derivation of a Distributed Program in Event B

Alexei Iliasov, Linas Laibinis, Elena Troubitsyna, Alexander Romanovsky, Formal Derivation of a Distributed Program in Event B. In: Shengchao Qin, Zongyan Qiu (Eds.), Formal Methods and Software Engineering, 13th International Conference on Formal Engineering Methods, ICFEM 2011, Lecture Notes in Computer Science 6991, 420 – 436, Springer, 2011.

Abstract:

Achieving high dependability of distributed systems remains a major challenge due to complexity arising from concurrency and com- munication. There are a number of formal approaches to verification of properties of distributed algorithms. However, there is still a lack of methods that enable a transition from a verified formal model of com- munication to a program that faithfully implements it. In this paper we aim at bridging this gap by proposing a state-based formal approach to correct-by-construction development of distributed programs. In our approach we take a systems view, i.e., formally model not only application but also its environment – the middleware that supports it. We decompose such an integrated specification to obtain the distributed program that should be deployed on the targeted network infrastructure. To illustrate our approach, we present a development of a distributed leader election protocol.

BibTeX entry:

@INPROCEEDINGS{inpIlLaTrRo11a,
  title = {Formal Derivation of a Distributed Program in Event B},
  booktitle = {Formal Methods and Software Engineering, 13th International Conference on Formal Engineering Methods, ICFEM 2011},
  author = {Iliasov, Alexei and Laibinis, Linas and Troubitsyna, Elena and Romanovsky, Alexander},
  volume = {6991},
  series = {Lecture Notes in Computer Science},
  editor = {Qin, Shengchao and Qiu, Zongyan},
  publisher = {Springer},
  pages = {420 – 436},
  year = {2011},
  keywords = {formal modelling, distributed systems, Event B, refinement},
}

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

Publication Forum rating of this publication: level 1

Edit publication