Service-Oriented Development of Fault Tolerant Communicating Systems: Refinement Approach

Service-Oriented Development of Fault Tolerant Communicating Systems: Refinement Approach

Linas Laibinis, Elena Troubitsyna, Sari Leppänen
ISBN13: 9781466609129|ISBN10: 1466609125|EISBN13: 9781466609136
DOI: 10.4018/978-1-4666-0912-9.ch016
Cite Chapter Cite Chapter

MLA

Laibinis, Linas, et al. "Service-Oriented Development of Fault Tolerant Communicating Systems: Refinement Approach." Innovations in Embedded and Real-Time Systems Engineering for Communication, edited by Seppo Virtanen, IGI Global, 2012, pp. 297-319. https://doi.org/10.4018/978-1-4666-0912-9.ch016

APA

Laibinis, L., Troubitsyna, E., & Leppänen, S. (2012). Service-Oriented Development of Fault Tolerant Communicating Systems: Refinement Approach. In S. Virtanen (Ed.), Innovations in Embedded and Real-Time Systems Engineering for Communication (pp. 297-319). IGI Global. https://doi.org/10.4018/978-1-4666-0912-9.ch016

Chicago

Laibinis, Linas, Elena Troubitsyna, and Sari Leppänen. "Service-Oriented Development of Fault Tolerant Communicating Systems: Refinement Approach." In Innovations in Embedded and Real-Time Systems Engineering for Communication, edited by Seppo Virtanen, 297-319. Hershey, PA: IGI Global, 2012. https://doi.org/10.4018/978-1-4666-0912-9.ch016

Export Reference

Mendeley
Favorite

Abstract

Telecommunication systems must have a high degree of availability, that is, a 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 increase confidence in building correct software. However, to be used in practice, formal methods should be well integrated into existing development process. In this paper, the authors propose a formal model-driven approach to development of communicating systems. The authors formalize and extend the Lyra approach—a top-down service-oriented method for development of communicating systems. Lyra is based on transformation and decomposition of models expressed in UML2. The authors 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 phases. Moreover, this paper extends Lyra to integrate reasoning about fault tolerance in the entire development flow.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.