形式化语言B与UML／OCL的比较

该文介绍了形式化方法中B语言和UML／OCL语言,从软件开发生命周期的角度对B语言和OCL语言进行了比较,归纳了这两种形式化语言的异同和各自的适用范围。     

OCL数据类型到B形式化规约的转换

研究了UML模型到B形式化规约的转换。提出了一套从OCL数据类型及定义在这些数据类型上的操作到BAMN的转换规则。OCL的Boolean类型和Integer类型分别对应于B中的BOOL类型和Z类型；OCL中的String类型需用B抽象机器重新定义新的数据类型Char_TYPE和String_TYPE来进行规约；OCL中的REAL类型采用B中的记录表达式进行近似模拟；OCL中的Collection类型（包括Set，Orderedset，Bag，Sequence）用B语言中的set，sequence，tree等进行近似模拟。     

基于OCL的模型转换语言

首先对模型驱动以及与模型驱动开发密切相关的元模型和模型转换两个问题进行了简要的说明,并介绍了模型转换框架的相关概念,然后对对象约束语言（OCL）进行了相关的讨论,并对基于OCL的模型转换语言的元模型进行了说明.最后,在讨论的基础之上,提出了基于对象约束语言的模型转换语言,为形式化及自动化的模型转换描述与实现提供了一种有效的方法.     

基于对象约束语言规格的变异分析

由于传统形式化语言的复杂性以及当前变异分析系统性能问题,基于规格的变异分析一直没有得到广泛的应用.介绍辅助UML建模的对象约束语言(OCL)和基于规格变异分析的基本理论.提出一种新型的OCL规格变异系统的设计方案,并详细描述了一些变异算子的具体实现.解决了传统变异系统的性能缺陷,提高了变异分析的实用性.     

基于OCL文法的测试用例自动生成方法研究

随着软件测试技术的飞速发展,很多自动生成和执行测试用例的方法的技术已经发展起来。对于自动生成测试用例的约束的形式化定义也有很多方法,其中,对象约束语言(OCL)就是其中最具代表性的。OCL能够弥补UML模型的不足,精确地定义约束条件。本文将着重介绍一种从OCL文法解析到约束条件分离的方法的研究结果,通过与OCL文法比较,解析输入的OCL文本,提取OCL表达式,构建约束条件树,实现约束条件分离,最终实现测试用例集的自动生成。     

基于OCL的本体模型校验方法

将集合关系理论与本体模型相结合,同时引入并扩展面向对象中的OCL(Object Constraint Language)语言,提出一种基于OCL的本体校验方法。该方法从大量本体模型中抽象出一个本体定义元模型ODM(Ontology Constraint Meta-model),该元模型基于集合关系理论,将本体模型划分为"实体相关元素"和"约束规则相关元素",并通过一系列OCL扩展函数来完成上述两种本体模型元素的形式化表示,以完成基于OCL的本体模型形式化校验。最后,通过宝钢信息共享平台车辆管理本体片段的本体模型校验实例,进一步讨论如何使用该模型校验方法实现本体模型的冲突检测和冲突消解。     

基于OCL文法的测试用例自动生成方法研究

随着软件测试技术的飞速发展，很多自动生成和执行测试用例的方法的技术已经发展起来。对于自动生成测试用例的约束的形式化定义也有很多方法，其中，对象约束语言（OCL）就是其中最具代表性的。OCL能够弥补UML模型的不足，精确地定义约束条件。本文将着重介绍一种从OCL文法解析到约束条件分离的方法的研究结果，通过与OCL文法比较，解析输入的OCL文本，提取OCL表达式，构建约束条件树，实现约束条件分离，最终实现测试用例集的自动生成。     

对象约束语言及其在精化PIM中的应用

为了应用精确、完备的PIM自动进行模型转换、校验及编译,分析了OCL元模型与UML元模型间的关系,在此基础上对OCL在精确化平台无关模型(PIM)方面的应用进行了研究,指出OCL面临的挑战,并对OCL的研究方向提出了几点建议。对象约束语言OCL可以对模型中的元素进行约束和查询,可以在MOF的任意一层上定义模型语言,还可以通过各种方法定义模型的转换规则。     

形式语言B与RSL的比较

本文介绍了形式化方法中B方法和RAISE方法,从软件开发生命周期的角度对B语言和RSL进行了比较,归纳了这两种形式化语言的异同和各自的适用范围。     

基于B语言的UML形式化方法

分析了目前主要的UML形式化方法及特点，提出了基于B语言的转换方法B2F(B-Based Formalization)，通过将UML模型转化为B抽象机描述实现UML的形式化描述和验证，并详细分析了基于B2F方法的UML类图的形式化，证明了该方法的可行性。     

Semantics of OCL specified with QVT

The Object Constraint Language (OCL) has been for many years formalized both in its syntax and semantics in the language standard. While the official definition of OCL’s syntax is already widely accepted and strictly supported by most OCL tools, there is no such agreement on OCL’s semantics, yet. In this paper, we propose an approach based on metamodeling and model transformations for formalizing the semantics of OCL. Similarly to OCL’s official semantics, our semantics formalizes the semantic domain of OCL, i.e. the possible values to which OCL expressions can evaluate, by a metamodel. Contrary to OCL’s official semantics, the evaluation of OCL expressions is formalized in our approach by model transformations written in QVT. Thanks to the chosen format, our semantics definition for OCL can be automatically transformed into a tool, which evaluates OCL expressions in a given context. Our work on the formalization of OCL’s semantics resulted also in the identification and better understanding of important semantic concepts, on which OCL relies. These insights are of great help when OCL has to be tailored as a constraint language of a given DSL. We show on an example, how the semantics of OCL has to be redefined in order to become a constraint language in a database domain.

Least-change bidirectional model transformation with QVT-R and ATL

QVT Relations (QVT-R) is the standard language proposed by the OMG to specify bidirectional model transformations. Unfortunately, in part due to ambiguities and omissions in the original semantics, acceptance and development of effective tool support have been slow. Recently, the checking semantics of QVT-R has been clarified and formalized. In this article, we propose a QVT-R tool that complies to such semantics. Unlike any other existing tool, it also supports meta-models enriched with OCL constraints (thus avoiding returning ill-formed models) and proposes an alternative enforcement semantics that works according to the simple and predictable “principle of least change.” The implementation is based on an embedding of both QVT-R transformations and UML class diagrams (annotated with OCL) in Alloy, a lightweight formal specification language with support for automatic model finding via SAT solving. We also show how this technique can be applied to bidirectionalize ATL, a popular (but unidirectional) model transformation language.     

An object-oriented operation-based approach to translation between MOF metaschemas

This paper proposes a new approach to the schema translation problem. We deal with schemas whose metaschemas are instances of the OMG’s MOF. Most metaschemas can be defined as an instance of the MOF; therefore, our approach is widely applicable. We leverage the well-known object-oriented concepts embedded in the MOF and its instances (object types, attributes, relationship types, operations, IsA hierarchies, refinements, invariants, pre- and postconditions, etc.) to define metaschemas, schemas and their translations.The main contribution of our approach is the extensive use of object-oriented concepts in the definition of translation mappings, particularly the use of operations (and their refinements) and invariants, both of which are formalized in OCL. Our translation mappings can be used to check that two schemas are translations of each other, and to translate one into the other, in both directions. The translation mappings are declaratively defined by means of pre- and postconditions and invariants, and they can be implemented in any suitable language. From an implementation point of view, by taking a MOF-based approach we have a wide set of tools available, including tools that execute OCL. By way of example, we have defined all schemas and metaschemas in this paper and executed all the OCL expressions in the USE tool.     

On OCL-based imperative languages

The Object Constraint Language (OCL) is a well-accepted ingredient in model-driven engineering and accompanying modeling languages such as UML (Unified Modeling Language) and EMF (Eclipse Modeling Framework) that support object-oriented software development. Among various possibilities, OCL offers the formulation of class invariants and operation contracts in form of pre- and postconditions, and side-effect free query operations. Much research has been done on OCL and various mature implementations are available for it. OCL is also used as the foundation for several modeling-specific programming and transformation languages. However, an intrusive way of embedding OCL into these language hampers us when we want to benefit from the existing achievements for OCL. In response to this shortcoming, we propose the language SOIL (Simple OCL-like Imperative Language), which we implemented in the UML and OCL modeling tool USE to amend its declarative model validation features. The expression sub-language of SOIL is identical to OCL. SOIL adds imperative constructs for programming in the domain of models. Thus by employing OCL and SOIL, it is possible to describe any operation in a declarative way and in an operational way on the modeling level without going into the details of a conventional programming language. In contrast to other similar approaches, the embedding of OCL into SOIL is done in a careful, non-intrusive way so that purity of OCL is preserved.     

A benchmark for OCL engine accuracy, determinateness, and efficiency

Since several years, the Object Constraint Language (OCL) is a central component in modeling and transformation languages like the Unified Modeling Language, the Meta Object Facility, and Query View Transformation. Consequently, approaches MDE (Model-Driven Engineering) depend on this language. OCL is present not only in areas influenced by the OMG but also in the Eclipse Modeling Framework (EMF). Thus the quality of OCL and its realization in tools seems to be crucial for the success of model-driven development. Surprisingly, up to now a benchmark for OCL to measure quality properties has not been proposed. This paper puts forward in the first part the concepts of a comprehensive OCL benchmark. Our benchmark covers (1) OCL engine accuracy (e.g., for the handling of the undefined value, the use of variables and the implementation of OCL standard operations), (2) OCL engine determinateness properties (e.g., for the collection operations ??any?? and ??flatten??), and (3) OCL engine efficiency (for data type and user-defined operations). In the second part, this paper empirically evaluates the proposed benchmark concepts by examining several OCL tools. The paper clarifies a number of differences in handling particular language features and under specifications in the OCL standard.     

基于EMF和OCL的MDA软件工程方法研究

随着基于模型的软件工程方法的兴起，模型逐渐地变为软件工程中的重要元素，介绍了OMG规范MOF、XMI和OCL及在Eclipse软件工程环境下的相关实现EMF，说明了统一建模语言UML的使用方式和存在的问题，介绍了如何用EMF和OCL来设计建模语言，比较了基于EMF的建模语言和基于EBNF的计算机语言之间的区别与联系，给出了结合模板和OCL的模型转换方法，通过把UML类模型转换到O／R映射框架说明了此方法的有效性，分析了MDA软件工程方法的重用机制。