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

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 different 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 communication 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.