• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Formal Verification of Consistency in Model-Driven Development of Distributed Communicating Systems and Communication Protocols

Dubravka Ilic, Elena Troubitsyna, Linas Laibinis, Sari Leppänen, Formal Verification of Consistency in Model-Driven Development of Distributed Communicating Systems and Communication Protocols. In: Tiziana andAnna Philippou Margaria (Ed.), IEEE 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006), 436-445, 2006.

Abstract:

Currently UML2 is widely used for modelling software-intensive systems. Model driven development of complex software typically starts from abstract, high-level UML2 models which specify the system from several dif¬ferent viewpoints. Abstract models are further refined into more detailed design models in successive development stages. While specifying various aspects and abstraction levels of such systems, we create a set of different models, which should be inter- and intra-consistent. In this paper we propose an approach to ensuring consistency in Lyra – a rigorous, service-oriented and model-based method for developing industrial telecommunication systems and communica¬tion protocols. We derive informal requirements to ensuring intra- and inter-consistency and then formalize them in the B Method. The formalization in B allows us to structure complex informal requirements and formally ensure intra- and inter-consistency of models created at various stages of the Lyra development.

BibTeX entry:

@INPROCEEDINGS{inpIlTrLaLe06a,
  title = {Formal Verification of Consistency in Model-Driven Development of Distributed Communicating Systems and Communication Protocols},
  booktitle = {IEEE 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006)},
  author = {Ilic, Dubravka and Troubitsyna, Elena and Laibinis, Linas and Leppänen, Sari},
  editor = {Margaria, Tiziana andAnna Philippou, Bernhard Steffen},
  pages = {436-445},
  year = {2006},
}

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

Edit publication