Development of a Modular Framework for Automatic Validation and Verification of UML/OCL Models

点击翻译按钮获取中文摘要

In order to face the steadily increasing complexity of today's software systems, the Unified Modeling Language (UML) together with the Object Constraint Language (OCL) has been established as a de-facto standard. UML/OCL allows for the description of the requirements, the behavior, and the structure of complex systems by hiding precise implementation details at the same time. As a result, UML/OCL enables to prove the correctness of a specified system already in the absence of an implementation. Considering the increasing time-to-market constraints, this aspect becomes particularly more and more important. As a consequence, several approaches aiming for the validation and verification of UML/OCL models have been developed in the recent past. However, they only address dedicated aspects such as single verification tasks or selected UML/OCL description means so far. Since practically relevant systems are usually specified through a variety of diagrams of different type, these approaches are often not applicable. Furthermore, existing verification approaches usually apply a single proof engine only. Hence, advantages of the different proof technologies have not been fully exploited so far. Because of this, methods for validation and verification of UML/OCL models are not established in current design tools.Within the proposed project, these problems should be addressed. The project aims at the development of a generic framework for the verification of UML/OCL models which (1) is based on automatic proof technologies, (2) supports different combinations of UML description means as well as verification tasks, and (3) allows for an easy exchange of proof engines. For this purpose, single diagram types or combinations of them as well as corresponding verification tasks shall not be treated separately. Instead, they shall be transformed into a base model which is powerful enough to represent diverse UML/OCL description means but only relies on atomic constructs in order to allow for a flexible usage within the framework.In the proposal, the general ideas of the planned framework are outlined. For the conduct of the project, the complementary expertise of two research groups is applied. The resulting framework shall be evaluated by means of a practically relevant example, namely the validation and verification of the so called XÖV standard.