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

为了面对当今软件系统日益增长的复杂性，统一建模语言（UML）和对象约束语言（OCL）已经被确立为事实上的标准。UML/OCL通过同时隐藏精确的实现细节，允许描述复杂系统的需求、行为和结构。因此，UML/OCL能够在没有实现的情况下证明指定系统的正确性。考虑到越来越多的上市时间限制，这方面变得越来越重要。因此，在最近的过去，已经开发了几种方法，旨在验证和验证UML/OCL模型。然而，他们只解决了专门的方面，如单一的验证任务或选择UML/OCL描述手段到目前为止。由于实际相关的系统通常通过不同类型的各种图表来指定，因此这些方法通常不适用。此外，现有的验证方法通常仅应用单个证明引擎。因此，不同的证明技术的优点还没有得到充分利用。因此，在目前的设计工具中还没有建立UML/OCL模型的确认和验证方法，这些问题需要在项目中得到解决。该项目旨在开发一个通用框架，用于验证UML/OCL模型，该框架（1）基于自动证明技术，（2）支持UML描述方法和验证任务的不同组合，（3）允许轻松交换证明引擎。为此，不应单独处理单一图表类型或其组合以及相应的验证任务。相反，它们应被转换成一个基本模型，这是强大到足以表示不同的UML/OCL描述手段，但只依赖于原子结构，以允许在框架内灵活使用。为了开展该项目，利用了两个研究小组的互补专门知识。由此产生的框架应通过一个实际相关的例子进行评估，即所谓的XÖV标准的确认和验证。

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.