A UML-based static verification framework for security

Secure software engineering is a new research area that has been proposed to address security issues during the development of software systems. This new area of research advocates that security characteristics should be considered from the early stages of the software development life cycle and should not be added as another layer in the system on an ad-hoc basis after the system is built. In this paper, we describe a UML-based Static Verification Framework (USVF) to support the design and verification of secure software systems in early stages of the software development life-cycle taking into consideration security and general requirements of the software system. USVF performs static verification on UML models consisting of UML class and state machine diagrams extended by an action language. We present an operational semantics of UML models, define a property specification language designed to reason about temporal and general properties of UML state machines using the semantic domains of the former, and implement the model checking process by translating models and properties into Promela, the input language of the SPIN model checker. We show that the methodology can be applied to the verification of security properties by representing the main aspects of security, namely availability, integrity and confidentiality, in the USVF property specification language.     

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.     

用UML与Petri网为智能代理建模

统一建模型语言（UML）已经成为软件系统的分析与设计的标准工具，但由它扩充而成的代理统一建模型语言（AUML）还没变成一个标准，目前的AUML规格说明还有很多的局限性，还不能胜任多代理系统的开发．Petri网是仿真、验证软件系统执行的正确性与有效性的形式化工具．本文主要分析当前AUML规格说明和Petri网概念．找出它们之间的结合点，提出用Petri网扩充AUML的方法．将其应用于多代理系统的开发，就能实施之前运用Petri网进行系统的正确性与有效性验证．     

On challenges of model transformation from UML to Alloy

The Unified Modeling Language (UML) is the de facto language used in the industry for software specifications. Once an application has been specified, Model Driven Architecture (MDA) techniques can be applied to generate code from such specifications. Since implementing a system based on a faulty design requires additional cost and effort, it is important to analyse the UML models at earlier stages of the software development lifecycle. This paper focuses on utilizing MDA techniques to deal with the analysis of UML models and identify design faults within a specification. Specifically, we show how UML models can be automatically transformed into Alloy which, in turn, can be automatically analysed by the Alloy Analyzer. The proposed approach relies on MDA techniques to transform UML models to Alloy. This paper reports on the challenges of the model transformation from UML class diagrams and OCL to Alloy. Those issues are caused by fundamental differences in the design philosophy of UML and Alloy. To facilitate better the representation of Alloy concepts in the UML, the paper draws on the lessons learnt and presents a UML profile for Alloy.     

一种基于描述逻辑的UML模型验证方法

针对UML模型中可能会存在的概念不一致、概念冗余等语义一致性问题,该文提出一种基于描述逻辑的UML模型形式化与模型验证方法。该方法首先采用描述逻辑的子系统SHOIN（D）形式化描述UML类图、状态图以及活动图的基本模型构造,进而将UML模型转换为相应的描述逻辑本体,最终借助现有的本体推理机制验证UML模型的语义一致性问题。该方法可以为下一代的软件CASE工具实现软件模型自动推理和验证提供一种可选的技术方案。     

基于同态映射的从UML导出可综合Verilog算法

UML建模因其可显著提高开发效率和代码质量已经成为软件开发领域的一大热点，而硬件设计的日益复杂性也要求我们在更高层次抽象上分析和验证系统行为，故更精细的系统级建模方法变得日趋重要。本文构建了UML元模型与可综合Verilog间的同态映射，定义了一个从UML模型子集导出可综合Verilog描述的算法，为UML模型对于建模硬件系统提供了形式化的语义，从而使运用UML进行硬件系统级建模和系统级上验证系统性能和功能正确性成为可能。     

Knowledge and software modeling using UML

Ontology can be considered as a comprehensive knowledge model which enables the developer to practice knowledge, instead of code, reuse. In the development of knowledge-based systems, different modeling languages are employed at different stages of the development process. By using a common modeling language for the knowledge and software models, knowledge instead of software reuse can be achieved. We illustrate the process by first presenting an ontology developed for an industrial domain and then investigate Unified Modeling Language (UML) as an ontology modeling tool. Since any model expressed in UML can be translated into a software model, the transition from the knowledge model to system implementation is better supported with the proposed approach. The industrial domain of selecting a remediation technique for petroleum contaminated sites is adopted for the illustration case study.     

基于对象着色Petri网的UML模型研究

UML广泛应用于软件建模,但缺乏有效的模型检测的方法,使用形式化方法对UML模型进行分析,可以发现UML模型的设计问题,提高UML模型的质量。对象着色Petri网是一种拥有接口库所的模块化着色Petri网,既是一种图形化建模工具,又是具有严格的语法语义定义的形式化方法。通过引入事件托肯,改进了将UML模型转换为对象着色Petri网的方法,结合实例将UML状态图和协作图映射为对象着色Petri网模型。并用着色Petri网的方法和工具对模型进行了分析,验证了模型的一系列性质。     

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.     

安全苛求软件需求规格中的安全特性验证方法

针对自然语言描述的安全苛求软件需求规格中安全特性不准确、不一致等问题,提出一种基于UMLsec安全特性验证方法。该方法在UML需求模型类图和顺序图的基础上,为核心类的安全特性自定义构造型、标记和约束,完成UMLsec模型构建;之后,使用设计实现的UMLsec支持工具对安全特性进行自动验证。实验结果表明,该方法能准确描述安全苛求软件需求规格的安全特性,同时可以自动验证安全特性是否满足安全需求。     

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.     

Verification of real‐time systems design

The main objective of this paper is to present an approach to accomplish verification in the early design phases of a system, which allows us to make the system verification easier, specifically for those systems with timing restrictions. For this purpose we use RT‐UML sequence diagrams in the design phase and we translate these diagrams into timed automata for performing the verification by using model checking techniques. Specifically, we use the Object Management Group's UML Profile for Schedulability, Performance, and Time and from the specifications written using this profile we obtain the corresponding timed automata. The ‘RT‐UML Profile’ is used in conjunction with a very well‐known tool to perform validation and verification of the timing needs, namely, the UPPAAL tool, which is used to simulate and analyze the behaviour of real‐time dynamic systems described by timed automata. Copyright © 2009 John Wiley & Sons, Ltd.     

一种软件自适应UML建模及其形式化验证方法

软件自适应的建模和形式化验证是提高自适应软件开发效率、保证自适应软件可靠性的基础,现有研究中软件自适应可视化建模与形式化建模相隔离,一定程度上阻碍了自适应软件的开发.为此,提出MV4SAS的方法,将可视化的UML与严格化的时间自动机相结合,用于软件自适应的建模和形式化验证.首先,应用UML扩展机制引入新的构造型、标记值和约束条件,定义软件自适应建模设施,在此基础上构造软件自适应结构模型和行为模型;然后,根据定义好的转换算法将软件自适应行为模型转换为时间自动机网络,建立软件自适应形式化模型;最后,定义一组软件自适应形式化验证性质,并利用模型检测工具UPPAAL验证软件自适应模型的可靠性.案例研究表明,该方法可有效降低软件自适应建模和验证的复杂度,提高软件自适应的建模效率和模型可靠性.     

实时软件系统开发技术

分析了开发实时系统和实时软件系统的特殊性，讨论了传统实时软件系统开发技术(包括RTSA技术、DARTS技术、JSD技术、NRL方法、OOA＆OOD技术等)，并比较了它们各自的优缺点．详细讨论了面向对象技术在实时软件系统开发中的应用，对统一建模语言(UML)在实时软件系统中的应用也进行了深入分析和讨论．在分析了实时UML(UML-RT)的不足之后，提出了融合UML和CPN的实时软件开发技术，并用一个实例说明了如何利用该技术进行实时软件开发．     

GUIDE: Games with UML for interactive design exploration

In this paper we present our design tool GUIDE, which allows the user to explore a design in UML interactively by playing a game. The game incorporates both the design model and a specification of what it means for the design to be correct. The central idea of this approach is that the designer can increment the game during a play and gradually add more detail to it. Specification and design are refined by repeated plays of the game. The designer stops playing when design and specification are detailed enough for his purpose and match each other. The interactive game approach helps to cope with incompleteness and informal definition of UML models, which make strictly formal verification techniques difficult. The designer may resolve these problems when they arise during a play or let the GUIDE tool determine how the play should proceed. We discuss the potential impact of GUIDE and tools like it on software development.     

Reasoning about UML/OCL class diagrams using constraint logic programming and formula

Model Driven Engineering promotes the use of models as the main artifacts in software and system development. Verification and validation of models are key activities to ensure the quality of the system under development. This paper presents a framework to reason about the satisfiability of class models described using the Unified Modeling Language (UML). The proposed framework allows us to identify possible design flaws as early as possible in the software development cycle. More specifically, we focus on UML Class Diagrams annotated with Object Constraint Language (OCL) invariants, which are considered to be the main artifacts in Object-Oriented analysis and design for representing the static structure of a system. We use the Constraint Logic programming (CLP) paradigm to reason about UML Class Diagrams modeling foundations. In particular, we use Formula as a model-finding and design space exploration tool. We also present an experimental Eclipse plug-in, which implements our UML model to Formula translation proposal following a Model Driven Architecture (MDA) approach. The proposed framework can be used to reason, validate, and verify UML Class Diagram software designs by checking correctness properties and generating model instances using the model exploration tool Formula.     

Validating UML and OCL models in USE by automatic snapshot generation

We study the testing and certification of UML and OCL models as supported by the validation tool USE. We extend the available USE features by introducing a language for defining properties of desired snapshots and by showing how such snapshots are generated. Within the approach, it is possible to treat test cases and validation cases. Test cases show that snapshots having desired properties can be constructed. Validation cases show that given properties are consequences of the original UML and OCL model.     

运用UML为软件项目建模研究

UML作为软件工程领域的标准建模语言 ,受到工程界的广泛关注 ,但怎样运用UML来建模仍没有一个统一的标准。通过实例介绍了UML的结构和机制 ,结合建模工具RationalRose说明如何在软件开发过程中运用UML建模     

Test Synthesis from UML Models of Distributed Software

The object-oriented software development process is increasingly used for the construction of complex distributed systems. In this context, behavior models have long been recognized as the basis for systematic approaches to requirements capture, specification, design, simulation, code generation, testing, and verification. Two complementary approaches for modeling behavior have proven useful in practice: interaction-based modeling (e.g., UML sequence diagrams) and state-based modeling (e.g., UML statecharts). Building on formal V&V techniques, in this article we present a method and a tool for automated synthesis of test cases from scenarios and a state-based design model of the application, remaining entirely within the UML framework. The underlying "on the fly" test synthesis algorithms are based on the input/output labeled transition system formalism, which is particularly appropriate for modeling applications involving asynchronous communication. The method is eminently compatible with classical OO development processes since it can be used to synthesize test cases from the scenarios used in early development stages to model global interactions between actors and components, instead of these test cases being derived manually. We illustrate the system test synthesis process using an air traffic control software example