带OCL约束条件的类图到Object-Z规格说明的转换

如何提高软件的可靠性是目前软件研究领域的一个热点。将形式化方法和主流的软件开发方法相结合是一个可行的方法。本文研究UML语言和Object-Z语言相结合的方法,为主流的软件开发人员所使用的图形化规格说明技术与形式方法提供的精确的分析和验证技术架起了一座桥梁。本文定义如何将带0CL约束条件的类图转换到Object-Z规格说明的方法。这样不仅可以通过支持Object-Z语言的工具采对UML语言描述的系统性质进行验证和确认,而且能够帮助规格说明人员方便地构造Object-Z规格说明。     

基于JML的面向对象设计指导测试方法的研究与实现

面向对象的软件测试应该也只能被设计所指导.提出了一种方案:在使用UML进行面向对象的设计阶段为类和方法加入OCL约束,然后由一种转换工具将带有OCL约束的UML类图转换为带有JML(Java建模语言,Java Modeling Language)注解的Java类代码框架,就可以利用JML丰富的支撑工具进行调试和自动测试,从而实现了设计指导测试的思想.研究了OCL到JML的转换机制,并给出了基于Rational Rose的转换工具JML-AddIn的实现框架.     

OCL2Trigger: Deriving active mechanisms for relational databases using Model-Driven Architecture

Transforming integrity constraints into active rules or triggers for verifying database consistency produces a serious and complex problem related to real time behaviour that must be considered for any implementation. Our main contribution to this work is to provide a complete approach for deriving the active mechanisms for Relational Databases from the specification of the integrity constraints by using OCL. This approach is designed in accordance with the MDA approach which consists of transforming the specified OCL clauses into a class diagram into SQL:2003 standard triggers, then transforming the standard triggers into target DBMS triggers. We believe that developing triggers and plugging them into a given model is insufficient because the behaviour of such triggers is invisible to the developers, and therefore not controllable. For this reason, a DBMS trigger verification model is used in our approach, in order to ensure the termination of trigger execution. Our approach is implemented as an add-in tool in Rational Rose called OCL2Trigger.     

高性能程控三相交流功率源的研制

提出了用于计量和测试产品性能的一种高性能程控三相交流功率源的设计方法.采用了SPWM逆变激励及OCL功放的功率输出,高性能的单片机加上CPLD和锁相环的配合,实现了功率源三相电压电流大小、相位和频率的任意调整,能产生既不平衡又不对称的功率信号输出.实验证明输出波形失真度小于0.7%,精度和稳定度优于0.5%,符合0.1级标准.     

一种支持MDA的UML类图到RDB模型的转换方法

UML被MDA用来描述各种模型,成为建模语言事实上的标准。但是,由于UML类图中缺少对关系数据库的实现的约束,使得类图转换到的关系数据库模型不唯一,不能充分体现设计者对数据库的设计意图。这不利于MDA中PIM模型和关系PSM模型的双向转换。为解决以上问题,本文提出一种通过添加构造型和OCL约束来扩展UML类图的方法,以加强类图中数据之间的关系及约束,使PIM模型能够唯一地转换到PSM模型。最后,采用QVT模型转换方法将扩展后的UML类图转换到关系数据库模型,并结合例子给出了UML类图的关联、继承、组合和聚合关系等到关系数据库模型的转换规则和方法。利用本方法可以使UML类图到关系数据库模型的转换结果唯一。     

Specification of temporal properties with OCL

The Object Constraint Language (OCL) is widely used to express static constraints on models and object-oriented systems. However, the notion of dynamic constraints, controlling the system behavior over time, has not been natively supported. Such dynamic constraints are necessary to handle temporal and real-time properties of systems.In this paper, we first add a temporal layer to the OCL language, based syntactically on Dwyer et al.'s specification patterns. We enrich it with formal scenario-based semantics and integrate it into the current Eclipse OCL plug-in. Second, we translate, with a compositional approach, OCL temporal properties into finite-state automata and we connect our framework to automatic test generators. This way, we create a bridge linking model driven engineering and usual formal methods.     

A model-driven runtime environment for Web applications

A large part of software development these days deals with building so-called Web applications. Many of these applications are data-base-powered and exhibit a page layout and navigational structure that is close to the class structure of the entities being managed by the system. Also, there is often only limited application-specific business logic. This makes the usual three-tier architectural approach unappealing, because it results in a lot of unnecessary overhead. One possible solution to this problem is the use of model-driven architecture (MDA). A simple platform-independent domain model describing only the entity structure of interest could be transformed into a platform-specific model that incorporates a persistence mechanism and a user interface. Yet, this raises a number of additional problems caused by the one-way, multi-transformational nature of the MDA process. To cope with these problems, the authors propose the notion of a model-driven runtime (MDR) environment that is able to execute a platform-independent model for a specific purpose instead of transforming it. The paper explains the concepts of an MDR that interprets OCL-annotated class diagrams and state machines to realize Web applications. It shows the authors' implementation of the approach, the Infolayer system, which is already used by a number of applications. Experiences from these applications are described, and the approach is compared to others. This is an extended and revised version of a paper originally presented at the UML 2003 conference in San Francisco [1]. The second author has been supported by the German Federal Ministry of Education and Research (BMBF), grant 08NM098.     

An analysis of metamodeling practices for MOF and OCL

The definition of a metamodel that precisely captures domain knowledge for effective know-how capitalization is a challenging task. A major obstacle for domain experts who want to build a metamodel is that they must master two radically different languages: an object-oriented, MOF-compliant, modeling language to capture the domain structure and first order logic (the Object Constraint Language) for the definition of well-formedness rules. However, there are no guidelines to assist the conjunct usage of both paradigms, and few tools support it. Consequently, we observe that most metamodels have only an object-oriented domain structure, leading to inaccurate metamodels. In this paper, we perform the first empirical study, which analyzes the current state of practice in metamodels that actually use logical expressions to constrain the structure. We analyze 33 metamodels including 995 rules coming from industry, academia and the Object Management Group, to understand how metamodelers articulate both languages. We implement a set of metrics in the OCLMetrics tool to evaluate the complexity of both parts, as well as the coupling between both. We observe that all metamodels tend to have a small, core subset of concepts, which are constrained by most of the rules, in general the rules are loosely coupled to the structure and we identify the set of OCL constructs actually used in rules.     

On the verification of UML/OCL class diagrams using constraint programming

Assessment of the correctness of software models is a key issue to ensure the quality of the final application. To this end, this paper presents an automatic method for the verification of UML class diagrams extended with OCL constraints. Our method checks compliance of the diagram with respect to several correctness properties including weak and strong satisfiability or absence of constraint redundancies among others. The method works by translating the UML/OCL model into a Constraint Satisfaction Problem (CSP) that is evaluated using state-of-the-art constraint solvers to determine the correctness of the initial model. Our approach is particularly relevant to current MDA and MDD methods where software models are the primary artifacts of the development process and the basis for the (semi-)automatic code-generation of the final application.     

Refinement and retrenchment for programming language data types

Refinement is a well-established and accepted technique for the systematic development of correct software systems. However, for the step from already refined specification to implementation, a correct refinement is often not possible because the data types used in the specification respectively the implementation language differ. In this paper, we discuss this problem and its consequences, using the integer data types of Java as an example, which do not correctly refine the mathematical integers ℤ. We present a solution, which can be seen as a generalisation of refinement and a variant of retrenchment. It has successfully been implemented as part of the KeY software verification system. Received November 2004 Revised July 2005 Accepted July 2005 by Eerke A. Boiten, John Derrick, Graeme Smith and Ian Hayes