You are here: TUCS > PUBLICATIONS > Publication Search > Formal Service-Oriented Develo...
Formal Service-Oriented Development of Fault Tolerant Communicating Systems
Linas Laibinis, Elena Troubitsyna, Sari Leppänen, Johan Lilius, Qaisar Malik, Formal Service-Oriented Development of Fault Tolerant Communicating Systems. TUCS Technical Reports 764, Turku Centre for Computer Science, 2006.
Abstract:
Telecommunication 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 and system fault
tolerance should be ensured. Application of formal methods helps us to gain
confidence in building correct software. However, to be used in practice,
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 and extends 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 the Lyra service specification, decomposition and distribution
phases. Moreover, we extend Lyra to integrate reasoning about fault tolerance in
the entire development flow.
Files:
Full publication in PDF-format
BibTeX entry:
@TECHREPORT{tLaTrLeLiMa06a,
title = {Formal Service-Oriented Development of Fault Tolerant Communicating Systems},
author = {Laibinis, Linas and Troubitsyna, Elena and Leppänen, Sari and Lilius, Johan and Malik, Qaisar},
number = {764},
series = {TUCS Technical Reports},
publisher = {Turku Centre for Computer Science},
year = {2006},
keywords = {communicating systems, service-oriented development, fault tolerance, UML, B Method},
ISBN = {952-12-1716-2},
}
Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)