Formal Verification of Consistency in Model-Driven Development of Distributed Communicating Systems and Communication Protocols
| Autor: | Elena Troubitsyna, Dubravka Ilic, Linas Laibinis, Sari Leppänen |
|---|---|
| Rok vydání: | 2006 |
| Předmět: |
Structure (mathematical logic)
business.industry Computer science Programming language B-Method computer.software_genre Consistency (database systems) Software Unified Modeling Language Software engineering business Communications protocol Formal verification computer computer.programming_language Abstraction (linguistics) |
| Zdroj: | ISoLA |
| DOI: | 10.1109/isola.2006.40 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|