Refinement and verification in component-based model-driven design

Modern software development is complex as it has to deal with many different and yet related aspects of applications. In practical software engineering this is now handled by a UML-like modelling approach in which different aspects are modelled by different notations. Component-based and object-oriented design techniques are found effective in the support of separation of correctness concerns of different aspects. These techniques are practised in a model-driven development process in which models are constructed in each phase of the development. To ensure the correctness of the software system developed, all models constructed in each phase are verifiable. This requires that the modelling notations are formally defined and related in order to have tool support developed for the integration of sophisticated checkers, generators and transformations. This paper summarises our research on the method of Refinement of Component and Object Systems (rCOS) and illustrates it with experiences from the work on the Common Component Modelling Example (CoCoME). This gives evidence that the formal techniques developed in rCOS can be integrated into a model-driven development process and shows where it may be integrated in computer-aided software engineering (CASE) tools for adding formally supported checking, transformation and generation facilities.     

Composing, analyzing and validating software models to assess the performability of competing design candidates

In a perfect world, verification and validation of a software design specification would be possible before any code was generated. Indeed, in a perfect world we would know that the implementation was correct because we could trust the class libraries, the development tools, verification tools and simulations, etc. These features would provide the confidence needed to know that all aspects (complexity, logical and timing correctness) of the design were fully satisfied (i.e., everything was right). Right in the sense that we built it right (it is correct with respect to its specification) and it solves the right problem. Unfortunately, it is not a perfect world, and therefore we must strive to continue to refine, develop and validate useful methods and tools for the creation of safe and correct software. This paper considers the analysis of systems expressed using formal notations. We introduce our framework, the modeling cycle, and motivate the need for tool supported rigorous methods. Our framework is about using systematic formal techniques for the creation and composition of software models that can further enable reasoning about high‐assurance systems. We describe several formal modeling techniques within this context (i.e., reliability and availability models, performance and functional models, performability models, etc.). This discussion includes a more precise discourse on stochastic methods (i.e., DTMC and CTMC) and their formulation. In addition, we briefly review the underlying theories and assumptions that are used to solve these models for the measure of interest (i.e., simulation, numerical and analytical techniques). Finally, we present a simple example that employs generalized stochastic Petri nets and illustrates the usefulness of such analysis methods. This revised version was published online in June 2006 with corrections to the Cover Date.     

Model-driven development of interactive groupware systems: Integration into the software development process

Modeling interactive groupware systems is a complex and multi-disciplinary task. It is necessary to provide designers and engineers with a set of methods, notations and tools to specify the different aspects to consider when designing this type of systems. In this work we present a methodological framework based on the integration of several notations and processes for modeling some of these aspects, in particular: interaction, collaboration and functionality. The objective of this work is to provide a more complete support to the design of groupware systems, considering different viewpoints and modeling perspectives of the several stakeholders involved in the development of such applications.     

一个MDA支撑工具的设计与实现

MDA是OMG提出的用于解决中间件集成问题的软件开发方法。MDA开发方法以系统模型作为软件开发的主线。在这样的开发过程中,强有力的模型转换支撑工具是MDA思想能够得到广泛应用的关键。而从平台无关模型PIM到平台相关模型PSM的转换工具尤其重要。描述了一个从PIM自动转换到PSM的工具的设计思想。工具使用EDOC profile的一个子集作为PIM的描述方法,使用J2EE作为目标平台。基于一组从PIM到J2EE平台上软件模型的转换规则,工具实现了从PIM到J2EE平台上的PSM的自动转换。     

Embedding requirements within Model-Driven Architecture

Model-Driven Architecture (MDA) brings benefits to software development, among them the potential for connecting software models with the business domain. This paper focuses on the upstream or Computation-Independent Model (CIM) phase of MDA. Our contention is that, whilst there are many models and notations available within the CIM phase, those that are currently popular and supported by the Object Management Group (OMG) may not be the most useful notations for business analysts nor sufficient to fully support software requirements and specification. Therefore, with specific emphasis on the value of the Business Process Modelling Notation (BPMN) for business analysts, this paper provides an example of a typical CIM approach before describing an approach that incorporates specific requirements techniques. A framework extension to MDA is then introduced, which embeds requirements and specification within the CIM, thus further enhancing the utility of MDA by providing a more complete method for business analysis.     

元建模技术研究进展

随着UML(unified modeling language)与MDA(model driven architecture)的兴起和流行,模型已经成为软件开发的核心制品,而模型重要性的提升使得建模语言以及定义建模语言的元模型逐渐成为软件开发中的一个核心要素.软件开发往往涉及多个领域,而不同的领域往往需要不同的建模语言及其建模工具.但是,手工地为不同的建模语言开发建模工具代价高昂.元建模技术是解决这个问题的方法之一,通过元建模,可以根据领域需要定制合适的元模型以定义领域建模语言,进而自动生成支持该建模语言的建模工具.大量的工程实践表明,与领域建模以及MDA相结合,元建模可以大幅度地提高软件开发效率,基于元建模的MDA比基于通用建模语言的MDA更具潜力.在最近的几年中,元建模及其相关技术发展迅猛,不但在技术上取得了长足的进步,而且在产业界也开始出现大规模的商业应用.总结了元建模的现有研究成果,分析和比较了现有元建模工具,探讨了元建模的可能发展方向.对元建模中存在的问题进行分析,并指出了可能的解决途径.     

基于模式的软件体系结构建模

文中给出了一种应用程序组件的领域建模方法,将组件静态方面的面向对象建模(类图)、组件行为或功能等动态方面的基于模式的建模(模式实例模型)与代码生成实现技术结合起来。并试图用模式描述组件体系结构风格,指导如何构造和组织一个系统。基于模式的软件体系结构设计方法可在很短的时间内创建各种组件,并通过改变模型中的抽象体系结构特性来满足应用程序中的体系结构要求,因而该方法是切实可行的。     

基于MDA的HLA仿真开发方法

为了解决HLA与其它中间件产品脱节、应用范围局限以及可重用的问题,将MDA方法引入HLA仿真设计中,尝试用MDA的模型思想提升HLA在整个软件生命周期内的可重用和互操作问题.通过将联邦成员的行为逻辑和集成代码分开,并用邦员的PIM映射行为逻辑,用SOM映射集成代码,建立PIM和SOM之间的对应关系并映射成接口代码,纵向条理化了联邦成员的开发,降低了联邦成员代码开发的复杂性和集成的难度.在对模型进行描述和映射时,分析了HLA对象模型和面向对象模型的区别和联系,建立了用MDA思想描述联邦成员的平台无关和平台相关模型的开发过程框架.     

Executable visual software modeling—the ZOOM approach

In this paper, we introduce a new executable visual software modeling approach called ZOOM (Z-Based Object Oriented Modeling). ZOOM extends a subset of UML-2 notations by providing UI modeling notations and a formal integration mechanism. ZOOM allows software modeling using both graphical and textual views for its structural, behavioral and UI models. Through a pre-defined event model, ZOOM integrates these models, and provides the runtime execution semantics for both code generation and software animation.     

Modeling real-time communication systems: Practices and experiences in Motorola

Visual modeling languages and techniques have been increasingly adopted for software specification, design, development, and testing. With the major improvements of UML 2.0 and tools support, visual modeling technologies have significant potential for simplifying design, facilitating collaborations, and reducing development cost. In this paper, we describe our practices and experiences of applying visual modeling techniques to the design and development of real-time wireless communication systems within Motorola. A model-driven engineering approach of integrating visual modeling with development and validation is described. Results, issues, and our viewpoints are also discussed.     

Comparative Evaluation of Model Transformation Specification Approaches

Model transformations have become a key element of model-driven software development, being used to transform platform-independent models to platform-specific models, to improve model quality, to introduce design patterns and refactorings, and to map models from one language to another. A large number of model transformation notations and tools exist. However, there are no guidelines on how to select appropriate notations for particular model transformation tasks, and no comprehensive comparisons of the relative merits of particular approaches. In this paper we provide a unified semantic treatment of model transformations, and show how correctness properties of model transformations can be defined using this semantics. We evaluate several approaches which have been developed for model transformation specification, with respect to their expressivity, complexity and support for verification, and make recommendations for resolving the outstanding problems concerning model transformation specification.     

MDA模型转换工具的研究

模型驱动架构MDA(Model Driven Architecture)是由OMG提出的,用于解决企业间应用集成问题的软件开发方法.自提出以来,MDA方法得到很多软件供应商和研究人员的强力支持,在工业界和学术界出现了很多支持MDA开发方法的模型转换工具.这些工具使用了不同技术和实现方法,各有千秋.这些工具的出现有力地促进了MDA开发方法的发展.从模型描述方法、模型转换方法和模型转换工具在软件生命周期中的位置等三个方面分析比较了当前流行的MDA模型转换工具.根据这些分析结果,进一步讨论了MDA模型转换工具的发展前景,并指出了进一步改进MDA模型转换工具的研究方向.     

A distributed and interactive system to integrated design and simulation for collaborative product development

The goal of applying collaborative product development in industry has raised the need to develop software tools supporting system integration and group collaboration. Current methods and tools mainly focus on the collaborative creation of design components and assemblies. However, few of them support the collaborative work in developing simulation models so that proposed design concepts and solutions can be evaluated by integrating expertise from several disciplines. The purpose of this research is to develop a distributed and interactive system on which designers and experts can work together to create, integrate and run simulations for engineering design. To develop such a system, a number of issues, e.g. effectiveness and efficiency of modeling work, the re-use of models, interaction and cooperation, accuracy of simulation, collaborative operation on models, etc., need to be addressed. This paper describes an open architecture to developing simulations for engineering design in a distributed and collaborative environment, identifies a set of key issues raised in this architecture, and presents the techniques employed in our solution.     

Writing and executing ODP computational viewpoint specifications using Maude

The Reference Model of Open Distributed Processing (RM-ODP) is a joint standardization effort by ITU-T and ISO/IEC for the specification of large open distributed systems. RM-ODP is becoming increasingly relevant now because the size and complexity of large distributed systems is challenging current software engineering methods and tools, and because international standards have become key to achieve the required interoperability between the different parties and organizations involved in the design and development of complex systems. RM-ODP defines five viewpoints for decomposing the design activity into separate areas of concern. One of the RM-ODP viewpoints, the computational viewpoint, focuses on the basic functionality of the system and its environment, independently of its distribution. Although several notations have been proposed to model the ODP computational viewpoint, either they are not expressive enough to faithfully represent all its concepts, or they tend to suffer from a lack of formal support. In this paper we introduce the use of Maude as a formal notation for writing and executing ODP computational viewpoint specifications. Maude is an executable rewriting logic language specially well suited for the specification of object-oriented open and distributed systems. We show how Maude offers a simple, natural, and accurate way of modeling the ODP computational viewpoint concepts, allows the execution of the specifications produced, and offers good tool support for reasoning about them.     

Simulating simulation-agnostic SysML models for enterprise information systems via DEVS

Systems Modeling Language (SysML) is used as the modeling infrastructure in systems engineering, especially for complex systems design, independently of the system domain. Simulation is a common method to perform system model verification, during the systems development process. However, simulation code generation and execution is not integrated within the system design activity, as it is facilitated by SysML. It is either conducted as an external activity, after system design, or it affects the system design environment and practices, according to specific simulators requirements.This paper presents how existing, simulation-agnostic SysML models from the domain of Enterprise Information System (EISs), can be transformed to executable simulation code and in addition how the simulation results can be incorporated into the source SysML model through the exploitation of Model Driven Architecture (MDA) principles and techniques. To this end, several tools and technologies are utilized, while the verification process is triggered and finalized via the system modeling environment. Adoption of MDA provides a solid, high-level infrastructure and tool availability to the proposed approach.     

一种基于对象序列图的组件交互协议设计方法

基于组件的软件开发(component-basedsoftwaredevelopment,简称CBSD)现已成为软件开发的主流范型之一,其关心的核心问题是组件标准化与组件间的互操作性.它在互操作方面被广泛采用的思想是,分离组件的功能与交互特征,使用独立部件-交互协议来协调组件之间的交互.基于这种思想,探讨运用UML(unifiedmodelinglanguage)的对象序列图(objectsequencediagram,简称OSD)方法进行组件交互协议设计的多个方面的研究,其中包括OSD规范的形式定义以及规范的静态和动态形式分析方法,并为开发组件交互协议提出了一个集成OSD可视化建模和形式分析技术的软件工具框架.     

Validation of static properties in unified modeling language models for cyber physical systems

Cyber physical systems (CPSs) can be found nowadays in various fields of activity. The increased interest for these systems as evidenced by the large number of applications led to complex research regarding the most suitable methods for design and development. A promising solution for specification, visualization, and documentation of CPSs uses the Object Management Group (OMG) unified modeling language (UML). UML models allow an intuitive approach for embedded systems design, helping end-users to specify the requirements. However, the UML models are represented in an informal language. Therefore, it is difficult to verify the correctness and completeness of a system design. The object constraint language (OCL) was defined to add constraints to UML, but it is deficient in strict notations of mathematics and logic that permits rigorous analysis and reasoning about the specifications. In this paper, we investigated how CPS applications modeled using UML deployment diagrams could be formally expressed and verified. We used Z language constructs and prototype verification system (PVS) as formal verification tools. Considering some relevant case studies presented in the literature, we investigated the opportunity of using this approach for validation of static properties in CPS UML models.