Where academic tradition
meets the exciting future

Formal Model-Driven Development of Communicating Systems

Linas Laibinis, Elena Troubitsyna, Sari Leppänen, Johan Lilius, Qaisar Malik, Formal Model-Driven Development of Communicating Systems. In: Kung-Kiu Lau, Richard Banach (Eds.), Proceedings of ICFEM 2005 - 7th International Conference on Formal Engineering Methods, Lecture Notes in Computer Science 3785, Springer, 2005.

Abstract:

Telecommunicating systems should have a high degree of availability, i.e., high probability of correct and timely provision of requested services. To achieve this, correctness of software for such systems should be ensured. Application of formal methods helps us to gain confidence in building correct software. However, to be used in practice, the formal methods should be well integrated into existing development process. In this paper we propose a formal model-driven approach to development of telecommunicating systems. Essentially their approach formalizes Lyra – a top-down service-oriented method for development of telecommunicating systems developed in Nokia. Lyra is based on transformation and decomposition of models expressed in UML2. We formalize Lyra in the B Method by proposing a set of formal specification and refinement patterns reflecting the essential models and transformations of Lyra. The proposed approach is illustrated by a case study.

BibTeX entry:

@INPROCEEDINGS{inpLaTrLeLiMa05b,
  title = {Formal Model-Driven Development of Communicating Systems},
  booktitle = {Proceedings of ICFEM 2005 - 7th International Conference on Formal Engineering Methods},
  author = {Laibinis, Linas and Troubitsyna, Elena and Leppänen, Sari and Lilius, Johan and Malik, Qaisar},
  volume = {3785},
  series = {Lecture Notes in Computer Science},
  editor = {Lau, Kung-Kiu and Banach, Richard},
  publisher = {Springer},
  year = {2005},
}

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

Publication Forum rating of this publication: level 1

Edit publication