Issues in distributed timed model checking

In this work we present Zeus, a distributed timed model checker that evolves from the TCTL model checker Kronos [13] and that currently can handle backwards computation of reachability properties [2] over timed automata [3].Zeus was developed following a software architecture-centric approach. Its conceptual architecture was conceived to be sufficiently modular to house several features such as a priori graph partitioning, synchronous and asynchronous computation, communication piggybacking, delayed messaging, and dead-time utilization.Surprisingly enough, early experiments pinpointed the difficulties of getting speedups using asynchronous versions and showed interesting results on the synchronous counterpart, although being intuitively less attractive.     

Using UML Action Semantics for model execution and transformation

The Unified Modelling Language (UML) lacks precise and formal foundations and semantics for several modeling constructs, such as transition guards or method bodies. These semantic discrepancies and loopholes prevent executability, making early testing and validation out of reach of UML tools. Furthermore, the semantic gap from high-level UML concepts to low-level programming constructs found in traditional object-oriented language prevents the development of efficient code generators.The recent Action Semantics (AS) proposal tackles these problems by extending the UML with yet another formalism for describing behavior, but with a strong emphasis on dynamic semantics. This formalism provides both, a metamodel integrated into the UML metamodel, and a model of execution for these statements. As a future OMG standard, the AS eases the move to tool interoperability, and allows for executable modeling and simulation.We explore in this paper a specificity of the AS: its applicability to the UML metamodel, itself a UML model. We show how this approach paves the way for powerful metaprogramming for model transformation. Furthermore, the overhead for designers is minimal, as mappings from usual object-oriented languages to the AS will be standardized.     

The KeY tool

KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an integrated manner. Formal specification is performed using the Object Constraint Language (OCL), which is part of the UML standard. KeY provides support for the authoring and formal analysis of OCL constraints. The target language of KeY based development is Java Card DL, a proper subset of Java for smart card applications and embedded systems. KeY uses a dynamic logic for Java Card DL to express proof obligations, and provides a state-of-the-art theorem prover for interactive and automated verification. Apart from its integration into UML based software development, a characteristic feature of KeY is that formal specification and verification can be introduced incrementally.     

Design issues and model for a distributed multi-user editor

The collaborative editing of documents is a very common task nowadays. Writing groups are often distributed over many locations because of the globalization of organizations and the increasing interdisciplinarity of tasks. Since many writers already use computers for their jobs, providing computer support for the collaborative writing process has been identified as an important goal. Numerous tools for computer supported collaborative writing have already emerged but in most cases have not come into widespread usage. In this article the requirements of users for a collaborative editor are analyzed. Providing as much flexibility as possible to the users is identified as a basic need. According to the requirements summary a model for a group editing environment is presented. The model covers cooperative work in local and wide area networks using synchronous and asynchronous cooperation. Finally, an application of the model is presented in the form of the multi-user editing environmentIris.     

元建模技术研究进展

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

Providing Architectural Languages and Tools Interoperability through Model Transformation Technologies

Many architectural languages have been proposed in the last 15 years, each one with the chief aim of becoming the ideal language for specifying software architectures. What is evident nowadays, instead, is that architectural languages are defined by stakeholder concerns. Capturing all such concerns within a single, narrowly focused notation is impossible. At the same time, it is also impractical to define and use a “universal” notation, such as UML. As a result, many domain-specific notations for architectural modeling have been proposed, each one focusing on a specific application domain, analysis type, or modeling environment. As a drawback, a proliferation of languages exists, each one with its own specific notation, tools, and domain specificity. No effective interoperability is possible to date. Therefore, if a software architect has to model a concern not supported by his own language/tool, he has to manually transform (and, eventually, keep aligned) the available architectural specification into the required language/tool. This paper presents DUALLy, an automated framework that allows architectural languages and tools interoperability. Given a number of architectural languages and tools, they can all interoperate thanks to automated model transformation techniques. DUALLy is implemented as an Eclipse plugin. Putting it in practice, we apply the DUALLy approach to the Darwin/FSP ADL and to a UML2.0 profile for software architectures. By making use of an industrial complex system, we transform a UML software architecture specification in Darwin/FSP, make some verifications by using LTSA, and reflect changes required by the verifications back to the UML specification.     

A Formal Object Approach to the Design of ZML

This paper addresses two issues: how formal object modeling techniques facilitate the XML application development and how XML technology helps formal/graphical software design process. In particular, the paper presents a XML/XSL approach to the development of a web environment for Z family languages (Z/Object-Z/TCOZ). The projection techniques and tools from object-oriented Z (in XML) to UML (in XMI) are developed using XSL Transformations (XSLT). Furthermore, object-oriented Z is used to specify and design the essential functionalities of the web environment and the projection tools to UML. In a sense, the paper also demonstrates a formal object approach to modeling XML applications.     

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.     

DSMDiff: a differentiation tool for domain-specific models

Model differentiation techniques, which provide the capability to identify mappings and differences between models, are essential to many model development and management practices. There has been initial research toward model differentiation applied to Unified Modeling Language (UML) diagrams, but differentiation of domain-specific models has not been explored deeply in the modeling community. Traditional modeling practice using the UML relies on a single fixed general-purpose language (i.e., all UML diagrams conform to a single metamodel). In contrast, Domain-Specific Modeling (DSM) is an emerging model-driven paradigm in which multiple metamodels are used to define various modeling languages that represent the key concepts and abstractions for particular domains. Therefore, domain-specific models may conform to various metamodels, which requires model differentiation algorithms be metamodel-independent and able to apply to multiple domain-specific modeling languages. This paper presents metamodel-independent algorithms and associated tools for detecting mappings and differences between domain-specific models, with facilities for graphical visualization of the detected differences.     

A Collaborative Approach for Multi-Threaded SAT Solving

The last decade progresses have led the Satisfiability Problem (sat) to be a great and competitive practical approach to solve a wide range of industrial and academic problems. Thanks to these progresses, the size and difficulty of the sat instances has grown significantly. Among the recent solvers, a few are parallel and most of them use the message passing paradigm. In a previous work by Vander-Swalmen et al. (IWOMP, 146–157, 2008), we presented a fine grain parallel sat solver designed for shared memory using OpenMP and named mtss, for Multi Threaded Sat Solver. mtss extends the “guiding path” notion and uses a collaborative approach where a rich thread is in charge of the search-tree evaluation and where a set of poor threads yield logical or heuristics information to simplify the rich task. In this paper, we extend the poor thread abilities of mtss and present extensive comparative results on random 3-sat problems. These new experimentations show that fine grained techniques associated to poor tasks within the framework of mtss can achieve very interesting speedup on multi-core processors.     

PKUMoDEL:模型驱动的开发和语言家族支持环境

OMG发布的UML语言家族和MDA架构促进了模型驱动软件开发的思想成为现实.建模语言版本升级或者面向不同领域的语言家族新增成员的不断出现,要求模型驱动开发环境除了使得模型成为软件开发生命周期中的主体之外,还应该具有元模型的定义和操纵能力.模型驱动的开发和语言家族支持环境PKUMoDEL是基于MOF的元建模环境和基于UML2.0的建模环境的集成体,很好地解决了诸如元模型的定义、扩展和评估、建模工具的自适应和演化、不同类型工具之间的集成、模型复用、从模型到运行环境的直接映射和部署等问题.     

Assessing the quality of metamodels

The complexity and diversity of modern software demands a variety of metamodel-based modeling languages for software development. Existing languages change continuously, and new ones are constantly emerging. In this situation, and especially for metamodel-based modeling languages, a quality assurance mechanism for metamodels is needed. This paper presents an approach to assessing the quality of metamodels. A quality model, which systematically characterizes and classifies quality attributes, and an operable measuring mechanism for effectively assessing the quality of metamodels based on the quality model, are presented, using UML as the main example.     

基于原语-模式的体系结构作战活动模型建模方法

为了理解、比较和集成由不同框架、不同工具及建模方法开发的体系结构,更好地支持以数据为中心的体系结构开发策略,提出了基于原语-模式的军事信息系统体系结构建模方法;依据XML的模型转换实现,重点研究了基于建模原语-模式的体系结构元模型与建模方法之间的语义映射规则;基于国际国防企业体系结构规范构建了作战活动模型(OV-5)的元模型,分别研究了OV-5的IDEF0建模和UML活动图建模的具体实现,构建了IDEF0及UML活动图与OV-5元模型数据元素严格的语义映射规则,规范了体系结构建模方法并保证了体系结构语义的精确性和一致性。     

基于XML的UML模型向AADL模型的自动转换

UML已经成为复杂系统建模的工业标准,并可借助代码自动生成工具实现从分析到编码的开发过程自动化;AADL具有精确的语义和严格的语法规范,可用于描述嵌入式实时系统的软、硬件体系结构,并能分析系统的功能及非功能属性。 UML和AADL模型的基本元对象有相互对应关系,并且两种模型的表示都能够采用标准的XML的交换格式。为充分发挥两种语言的优势,文中研究了UML模型向AADL模型的自动转换,以XML为媒介实现两种模型的元对象的对应转换,最终达到两种模型的转换,使用户在设计阶段能够结合运用AADL、UML工具的优点对系统进行分析。     

Semantische Prozessmodellierung – Konzeption und informationstechnische Unterstützung einer ontologiebasierten Repräsentation von Geschäftsprozessen

An extension of process modeling languages is designed which allows representing the semantics of model element labels which are formulated in natural language by using concepts of a formal ontology. This combination of semiformal models with formal ontologies will be characterized as semantic process modeling. The approach is exemplarily applied to the languages EPC (Event-driven Process Chain), BPMN (Business Process Modeling Notation) and OWL (Web Ontology Language) and is generalized by means of an information model. The proposed formalization of the semantics of individual model elements in conjunction with the usage of inference engines allows the improvement of query functionalities in modeling tools and enables new possibilities of model validation. The integration of the approach in the IT-based work environments of modelers is demonstrated by a system architecture and a prototypical implementation. Evidently, advantages in the areas of modeling, model management, business/IT alignment, and compliance can be achieved by the application of modeling tools augmented with semantic technologies.     

UML可视化建模工具中模型一致性检查机制的研究与实现

采用统一建模语言UML进行系统建模的过程中,模型一致性的建立和维护是正确建模的必要前提。但单靠人工检查的方式来保证模型的正确性,不仅给开发人员造成很大负担,而且容易出现差错或遗漏。因此,在UML可视化建模工具中提供模型一致性自动检测和维护机制至关重要。本文对UML主要模型图之间的关系进行了分析,识别出这些图之间的一些基本的一致性规则;在此基础上,提出了UML可视化建模工具中模型一致性检查机制的实施框架,并对实现该框架的主要思路进行了详细介绍。     

Integrating Data Flow Equations with UML/Realtime

Object-oriented (OO) modeling languages, tools, and methods more and more attract the interest of embedded (real-time) system developers. This is especially true if embedded (real-time) system software has to cooperate with interactive multimedia software, as it is more and more the case in automotive systems. It is still an open question whether and how the standard OO modeling language UML and its accompanying tools have to be adapted to the regarded application domain. This paper evaluates the development of a rapid prototype for an air condition controller with the popular CASE tool Rational Rose/RT^®. We point out some weaknesses of the presented solution and propose an extension to Rose/RT^®, which overcomes the weaknesses by combining Rose/RTs UML dialect with data flow equations.     

How are UML class diagrams built in practice? A usability study of two UML tools: Magicdraw and Papyrus

Software modeling is a key activity in software development, especially when following any kind of Model Driven Software Engineering (MDSE) process. In this context, standard modeling languages, like the Unified Modeling Language (UML), and tools for supporting the modeling activities become essential.The aim of this study is to analyze how modelers build UML models and how good modeling tools are in supporting this task. Our goal is to draw some useful lessons that help to improve the (UML) modeling process both by recommending changes on the tools themselves and on how UML is taught so that theory and practice of UML modeling are better aligned.Our study employs two research approaches. The main one is an empirical experiment (which analyzes screen recordings registered by undergraduate students during the construction of a UML class diagram). An analytical analysis complements the previous experiment. The study focuses on the most frequent type of UML diagram, the class diagram, and on two tools widely used by the modeling community: MagicDraw and Papyrus.