基于对象的分布式实时系统调度模型研究

为了解决分布式实时系统有关分配和调度等问题，给出并用形式化方法描述了一种基于对象分布式实时系统调度的通用模型。该模型包括表示时限的绝对时间约束，表示周期属性的周期约束，表示各种前趋关系和同步要求的相对时间约束以及保证资源使用一致性的一致性约束，此外该模型克服了以往模型不能在应用系统的逻辑和功能部件上描述系统实时的约束的不足，允许从方法和活动上描述所需的约束，降低了单一约束描述的繁杂程度，为了能够使用现有调度算法进行任务调度，讨论了约束转换的问题，给出了高层约束到底层约束的转换规则和相应的转换算法。     

一种基于规则的模型转换方法*

尽管模型驱动开发(MDD)代表软件工程的发展方向,但是目前MDD还缺乏一套完整的转换规则描述方法和相应的实现机制,难以实现模型的自动转换。为此定义了一个平台独立模型到平台相关模型的转换框架,采用UML活动图说明模型转换的实现机制;基于OCL定义了转换规则的表示法,并结合UML模型到Java模型的转换给出了转换规则的定义。最后在一个具体的实例中验证了此方法的合理性和易用性。     

支持模型驱动开发的软构件形式化描述方法

针对模型驱动的软件开发(MDSD)中语义特性保持的描述和验证等问题,基于类型范畴理论的形式化框架和进程代数理论,提出了一种软件结构模型的形式化描述方法。在此基础上对模型转换前后构件规范之间应满足的语义约束进行了深入的分析和探讨,从图表结构、端口与配置约束、外部行为以及可替换性等四个方面对特性约束保持的问题进行了描述,并建立了相应的判定标准。该方法能为模型之间转换规则的定义提供指导,并为模型转换的效果分析和正确性验证提供依据。应用研究表明,该方法使得构件模型的语义描述能力显著增强,可作为已有软件建模方法的一个有效补充。     

模型驱动开发中模型演化语法和语义特性研究

模型演化由一系列复杂的变化活动组成,要遵循一定的约束以保持模型的某些特性。以一个实例描述模型演化的过程,并以集值映射为基础,定义模型成分与语义域的映射,通过定义模型演化的语义函数,研究模型演化的语法和语义性质,包括特性保持、一致性、等价性和吸收性等。     

关键循环到可重构阵列映射中的时序参数分析

通过定义算法关键循环到可重构阵列映射的建立时间、保持时间等核心时序参数,分析存储器带宽有限、算法数据流图拓扑不规则等实际问题,给出配置时序模型的优化算法,提出路径特征等参数的描述形式,为可重构自动编译提供新的处理方式。验证结果表明,在视频算法H.264关键循环deblocking的映射过程中,该优化映射方法使得性能在原有基础上提升43%。     

元模型层次的UML动态子图到Coq形式规范的转换

UML动态子图主要包括序列图和状态图等,它们在描述系统的行为方面应用广泛,但是半形式化的语义使它们不能直接进行形式化验证。Coq是目前主流的交互式定理证明器,用形式化的Coq规范来描述UML动态子图模型,可以在此基础上进行对模型的属性进行验证等工作。基于现有工作,提出将UML动态子图模型转换为Coq形式规范的框架,在元模型层次给出状态图和序列图的转换规则,介绍算法和原型工具实现。这种元模型层次的转换方法,保证了转换前后的语法正确性,为进一步分析验证提供了基础。     

软件体系结构的属性图文法描述及其约束验证*

在前人工作的基础上,使用了一种利于约束检查和属性刻画的属性图文法,该方法形式地描述了体系结构及其演化;接着给出了一个算法检查演化动作是否会破坏体系结构约束.在对属性图文法系统AGG的图形解析器进行定制和改进的基础上,设计并实现了体系结构自动检查器.该检查器已应用于面向体系结构的服务集成开发平台Artemis-ARC系统中.     

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

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

UML活动图到Petri网的转换方法及实现研究

统一建模语言UML缺乏形式化语义,由其描述的模型难以进行动态的分析和验证。而Petri网在具有丰富而严格语义的同时,又有严谨的数学分析方法。综合运用Petri网和UML能够提高软件描述的全面性、一致性、精确性和完整性。研究了UML活动图向Petri网的转换规则,并依据转换规则实现了模型转换工具APConverter。此工具能有效地将活动图转换为Petri网模型并生成PNML文件,进而更好地对UML模型进行分析和验证。     

加强信息安全风险评估工作的研究

针对目前异构数据库间通信的问题,提出了种基于XML的数据交换技术.在具本实现过程中,进一步研究了XML模式与关系模式相互转换的方法,并给出了转换算法和转换规则。同时对XML模式中的语义约束同关系模式中的完整性约束之间的相互转换方法进行了分析。     

Constraint—Preserving Architecture Transformations：A Graph Rewriting Approach

Architecture transformations are frequently performed during software design and maintenance.However this activity is not well supported at a sufficiently abstract level.In this paper,the authors characterize architecture transformations using using graph rewriting rules,where architectures are represented in graph notations,Architectures are usually required to satisfy certain constraints during evolution.Therefore a way is presented to construct the sufficient and necessary condition for a transformatio to preserve a constraint.The condition can be verified before the application of the transformation.Validated transformations are guaranteed not to violate corresponding constraints whenever applied.     

一种随机化的软件模型生成方法

模型转换是模型驱动开发的核心技术. 当要把模型转换用于工业生产时, 其性能成为影响这一技术成败的关键因素之一. 为了测试模型转换程序的性能, 需要能够快速地生成一组具有较大规模的模型数据用于作为测试的输入数据. 本文提出一种随机化的模型生成方法. 该方法能够根据元模型的定义以及用户输入的约束条件随机、正确地生成模型文件. 实验结果也表明, 本方法和其它方法相比具有更好的生成效率, 从而更加适合支持模型转换的性能测试.     

From UML/SPT models to schedulability analysis: approach and a prototype implementation using ATL

Model Driven Architecture (MDA) is a software development approach promoted by the OMG. MDA is based on two key concepts, models and model transformations. Several kinds of models are generally used throughout the development process to specify a software system and to support its analysis and validation. UML and its extensions, such as the UML profile for real-time systems (UML/SPT), are commonly used to define the structure and the behavior of software systems while other models, such as performance models or schedulability models, are more suitable for performance or schedulability analysis, respectively. In this paper we discuss a model transformation enabling the derivation of schedulability analysis models from UML/SPT models. As a proof of concepts, we present a prototype implementation of this model transformation using ATL. We provide a definition of the source and target metamodels using the metamodel specification language KM3 and we specify the transformation in an ATL module. We discuss the merits and limitations of our approach and of its implementation.     

Formal foundation of consistent EMF model transformations by algebraic graph transformation

Model transformation is one of the key activities in model-driven software development. An increasingly popular technology to define modeling languages is provided by the Eclipse Modeling Framework (EMF). Several EMF model transformation approaches have been developed, focusing on different transformation aspects. To validate model transformations with respect to functional behavior and correctness, a formal foundation is needed. In this paper, we define consistent EMF model transformations as a restricted class of typed graph transformations using node type inheritance. Containment constraints of EMF model transformations are translated to a special kind of graph transformation rules such that their application leads to consistent transformation results only. Thus, consistent EMF model transformations behave like algebraic graph transformations and the rich theory of algebraic graph transformation can be applied to these EMF model transformations to show functional behavior and correctness. Furthermore, we propose parallel graph transformation as a suitable framework for modeling EMF model transformations with multi-object structures. Rules extended by multi-object structures can specify a flexible number of recurring structures. The actual number of recurring structures is dependent on the application context of such a rule. We illustrate our approach by selected refactorings of simplified statechart models. Finally, we discuss the implementation of our concepts in a tool environment for EMF model transformations.     

Relating evolving business rules to software design

In order to remain useful, it is important for software to evolve according to the changes in its business environment. Business rules, which can be used to represent both user requirements and conditions to which the system should conform, are considered as the most volatile part in today's software applications. Their changes bring high impact on both the business processes and the software itself. In this paper, we present an approach that considers business rules as an integral part of a software system and its evolution. The approach transcends the areas of requirements specification and software design. We develop the Business Rule Model to capture and specify business rules, and the Link Model to relate business rules to the metamodel level of software design elements. The aim is to improve requirements traceability in software design, as well as minimizing the efforts of software changes due to the changes of business rules. The approach is demonstrated using examples from an industrial application.     

Adapting transformations to metamodel changes via external transformation composition

Evolution is inherent to software systemsbecause of the rapid improvement of technologies and business logic. As a software development paradigm, model driven engineering (MDE) is also affected by this problem. More concretely, being metamodels the cornerstone of MDE, their evolution impacts the rest of software artefacts involved in a development process, i.e., models and transformations. The influence over models has been tackled and partially solved in previous works. This paper focuses on the impact over transformations. We propose an approach to adapt transformations by means of external transformation composition. That is, we chain impacted transformations to particular adaptation transformations which deal with either refactoring/destruction changes or construction changes. Our approach semi-automatically generates such transformations by using the AtlanMod matching language, a DSL to define model matching strategies. To provide with a proof of concept for our proposal, we adapt transformations written in terms of object-relational database metamodels when such metamodels evolve in time.     

Using model transformation to refactor use case models based on antipatterns

Use Case modeling is a popular technique for documenting functional requirements of software systems. Refactoring is the process of enhancing the structure of a software artifact without changing its intended behavior. Refactoring, which was first introduced for source code, has been extended for use case models. Antipatterns are low quality solutions to commonly occurring design problems. The presence of antipatterns in a use case model is likely to propagate defects to other software artifacts. Therefore, detection and refactoring of antipatterns in use case models is crucial for ensuring the overall quality of a software system. Model transformation can greatly ease several software development activities including model refactoring. In this paper, a model transformation approach is proposed for improving the quality of use case models. Model transformations which can detect antipattern instances in a given use case model, and refactor them appropriately are defined and implemented. The practicability of the approach is demonstrated by applying it on a case study that pertains to biodiversity database system. The results show that model transformations can efficiently improve quality of use case models by saving time and effort.     

Component Verification with Automatically Generated Assumptions

Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. The typical approach to verifying properties of software components is to check them for all possible environments. In reality, however, a component is only required to satisfy properties in specific environments. Unless these environments are formally characterized and used during verification (assume-guarantee paradigm), the results returned by verification can be overly pessimistic. This work introduces an approach that brings a new dimension to model checking of software components. When checking a component against a property, our modified model checking algorithms return one of the following three results: the component satisfies a property for any environment; the component violates the property for any environment; or finally, our algorithms generate an assumption that characterizes exactly those environments in which the component satisfies its required property. Our approach has been implemented in the LTSA tool and has been applied to the analysis of two NASA applications.This paper is an expanded version of Giannakopoulou et al. (2002).