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.