Linas Laibinis
Åbo Akademi University, Finland
Elena Troubitsyna
Åbo Akademi University, Finland
Sari Leppänen
Nokia Research Center, Finland
Download articlePublished in: NODES 09: NOrdic workshop and doctoral symposium on DEpendability and Security; Linköping; Sweden; April 27; 2009
Linköping Electronic Conference Proceedings 41:9, p. 67-76
Published: 2009-07-14
ISBN:
ISSN: 1650-3686 (print), 1650-3740 (online)
Telecommunication systems should have a high degree of availability; i.e.; high probability of correct provision of requested services. To achieve this; correctness of software for such systems and system fault tolerance should be ensured. In this paper we show how to formalise and extend Lyra – a top-down service-oriented method for development of communicating systems. In particular; we focus on integration of fault tolerance mechanisms into the entire Lyra development flow.
1. J.-R. Abrial. The B-Book. Cambridge University Press; 1996.
2. J.-R. Abrial. Extending B without Changing it (for Developing Distributed Systems). Proceedings of 1st Conference on the B Method; pp.169-191; Springer-Verlag; November 1996; Nantes; France.
3. Clearsy. AtelierB: User and Reference Manuals. Available at http://www.atelierb.societe.com/index uk.html.
4. L. Laibinis; E. Troubitsyna; S. Lepp¨anen; J.Lilius; and Q. Malik. Formal Service- Oriented Development of Fault Tolerant Communicating Systems. Rigorous Development of Complex Fault-Tolerant Systems; Lecture Notes in Computer Science; Vol.4157; chapter 14; pp.261-287; Springer-Verlag; 2006.
5. L. Laibinis; E. Troubitsyna; S. Lepp¨anen; J. Lilius; and Qaisar Malik. Formal Model- Driven Development of Communicating Systems. Proceedings of 7th International Conference on Formal Engineering Methods (ICFEM’05); LNCS 3785; Springer; November 2005.
6. S. Lepp¨anen; M. Turunen; and I. Oliver. Application Driven Methodology for Development of Communicating Systems. Forum on Specification and Design Languages; Lille; France; 2004.
7. Rigorous Open Development Environment for Complex Systems (RODIN). Deliverable D7; Event B Language; online at http://rodin.cs.ncl.ac.uk/.
8. Rigorous Open Development Environment for Complex Systems (RODIN). IST FP6 STREP project; online at http://rodin.cs.ncl.ac.uk/.