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. TUCS Technical Reports 691, Turku Centre for Computer Science, 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. An 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 communicating systems. Essentially our
approach formalizes Lyra – a top-down service-oriented method for
development of communicating systems. 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 – development of
the 3GPP positioning system.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tLaTrLeLiMa05a,
  title = {Formal Model-Driven Development of Communicating Systems},
  author = {Laibinis, Linas and Troubitsyna, Elena and Leppänen, Sari and Lilius, Johan and Malik, Qaisar},
  number = {691},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2005},
  ISBN = {952-12-1564-X},
}

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

Edit publication