Use of a lightweight formal method to model the static aspects of state machines

In this paper the author uses Alloy as a modeling language to model the elements that form a state machine and the rules that govern how they can be connected. In particular, the model proposed in this paper focuses in the static aspects of state machines. To analyze and detect design errors in the model, the Alloy analyzer was used. With the use of this tool, design errors can be detected very quickly. This tool can also generate instances of the model without making a line of code. The paper presents two models based on the formal approach: a graphical model and a textual model. The graphical model is used as an overview of the system while the textual model is used to establish further constraints on the graphical model.     

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（Unified Modeling Language)是一种标准的、功能强大的建模语言。以订单处理系统的分析和设计为例,详细介绍了UML（统一建模语言）的实际建模过程。     

基于C／S和B／S混合模式的银行业考试考务管理系统的设计

文章以中国银行业从业人员资格考试考务管理系统为例,描述应用UML进行考务管理系统建模的过程,并对其进行需求分析、总体设计和详细设计,最终采用面向对象的语言设计实现银行业从业人员资格考试考务管理系统。实践表明：本文所设计的考务管理系统开发周期短,系统的稳定性好、安全性高,并具有很强的可维护性和可重用性。     

基于AltaRica的故障自动化建模和分析

随着系统规模和复杂性的增加,系统安全性建模和分析技术在关键安全系统中得到了广泛应用.AltaRica是用于安全性分析的高级建模语言,AltaRica模型能够更好地反映系统功能和逻辑结构,消除传统安全性分析手段与系统设计的隔阂,提高安全性模型的可维护性和重用性.文章将AltaRica与计算机可视化建模技术相结合,开发了支...     

后勤财务管理系统的面向对象分析与设计

后勤财务管理系统是为后勤各实体企业化后实施行之有效的管理而建立的系统。统一建模语言UML是面向对象分析和设计过程中重要的建模工具,该语言可以对系统的不同层面进行描述。本文运用UML语言对系统软件进行了面向对象的分析与设计,探讨了静态结构建模和动态建模的方法。     

基于UML的糖尿病临床营养膳食配置专家系统的设计

统一建模语言(UML)是一种面向对象建模语言的标准。该文以糖尿病临床营养膳食配置专家系统为原型,利用UML的技术和方法,对系统进行分析和设计。     

AADL+: a simulation-based methodology for cyber-physical systems

AADL (architecture analysis and design language) concentrates on the modeling and analysis of application system architectures. It is quite popular for its simple syntax, powerful functionality and extensibility and has been widely applied in embedded systems for its advantage. However, it is not enough for AADL to model cyber-physical systems (CPS) mainly because it cannot be used to model the continuous dynamic behaviors. This paper proposes an approach to construct a new sublanguage of AADL called AADL+, to facilitate the modeling of not only the discrete and continuous behavior of CPS, but also interaction between cyber components and physical components. The syntax and semantics of the sublanguage are provided to describe the behaviors of the systems. What’s more, we develop a plug-in to OSATE (open-source AADL tool environment) for the modeling of CPS. And the plug-in supports syntax checking and simulation of the system model through linking with modelica. Finally, the AADL+ annex is successfully applied to model a lunar rover control system.     

基于UML的图书管理系统的建模过程

UML是一种建模语言,它取代软件界的众多分析和设计方法,已经成为被业界认可的标准建模语言,在软件领域和其他领域都起着举足轻重的作用。UML支持从需求分析、系统设计到具体实现的软件开发全过程。本文通过对图书管理系统的分析,介绍UML的基本概念和建模过程,从而说明UML在实际问题中的应用。     

Using the Alloy Analyzer to Verify Data Refinement in Z

In the development of critical systems, standards dictate that it is necessary to first design, construct and formally analyse abstract models of the system. Developers must then verify that the final implementation is consistent with these more abstract specifications.Z is an example of a state-based specification language. It has been shown to be effective in a variety of cases—indeed it was developed as part of a joint collaboration between Oxford University's PRG and IBM Hursley for the specification of the CICS system. However, Z's main weakness is that it does not have the necessary tool support: whilst there are associated type checkers, there is no tool for automatically verifying refinement in Z.The contribution of this paper is to show how data refinement in Z can be automatically verified using the Alloy Analyzer. The soundness and joint completeness of the simulation rules for Z have already been established: here we translate them to Alloy. We then show how data types expressed in Z can also be translated to Alloy, before presenting the assertions necessary for the Alloy Analyzer to identify the retrieve relation and hence verify refinement. We present a simple example in which the Alloy Analyzer successfully identifies the retrieve relation between two data types thereby verifying simulation and hence refinement. We conclude the paper with a discussion of the suitability of the Alloy Analyzer for such a task.     

基于UML的系统分析与设计框架

UML是一种标准的建模语言,但它并没有定义一个标准的开发过程.根据多年的教学科研和开发实践,提出一个基于UML的面向对象分析与设计框架,以用例为核心,描述软件系统的功能需求,静态结构,动态行为和物理结构4个方面.该框架展示了UML建模在系统开发中的应用,深入地研究建模过程中所用的模型图及其之间的关系,解决了开发过程中的模型平稳过渡问题,时面向对象分析与设计具有很强的指导性.     

电子图书在线出版系统的分析与设计

UML是可视化,规范定义、构造和文档化的建模语言,目前它已经成为面向对象软件系统分析与设计的必要工具。本文基于UML的面向对象系统分析及设计方法,完成电子图书在线出版系统的需求分析、建模与设计。     

UML在图书馆管理系统建模中的应用

统一建模语言(UML)是一种可视化的面向对象的建模语言,可用于对软件系统进行描述和构造软件的系统结构.本文介绍了UML的主要内容,并以图书馆管理系统为实例,探讨了应用UML建模机制,对系统的需求分析、详细设计及实现的不同阶段的建模过程.     

UML在印刷行业ERP建模中的应用

UML是一种基于面向对象技术的标准建模语言,它融入了软件工程领域的新思想、新方法和新技术,不仅支持面向对象的分析和设计,而且支持从需求分析到系统实现的软件开发的全过程.本文以印刷行业ERP系统中生产子系统的开发为例,详细讨论和分析了UML在印刷ERP系统建模中的应用和建模的关键技术.     

Clafer: unifying class and feature modeling

We present Clafer (class, feature, reference), a class modeling language with first-class support for feature modeling. We designed Clafer as a concise notation for meta-models, feature models, mixtures of meta- and feature models (such as components with options), and models that couple feature models and meta-models via constraints (such as mapping feature configurations to component configurations or model templates). Clafer allows arranging models into multiple specialization and extension layers via constraints and inheritance. We identify several key mechanisms allowing a meta-modeling language to express feature models concisely. Clafer unifies basic modeling constructs, such as class, association, and property, into a single construct, called clafer. We provide the language with a formal semantics built in a structurally explicit way. The resulting semantics explains the meaning of hierarchical models whereby properties can be arbitrarily nested in the presence of inheritance and feature modeling constructs. The semantics also enables building consistent automated reasoning support for the language: To date, we implemented three reasoners for Clafer based on Alloy, Z3 SMT, and Choco3 CSP solvers. We show that Clafer meets its design objectives using examples and by comparing to other languages.     

基于UML的混合流水线制造系统仿真软件设计

UML作为当前流行的一种标准建模语言,已越来越广泛地应用于各种应用领域的软件系统设计。该文通过运用UML对混合流水线制造系统仿真软件的设计,阐明UML在系统仿真软件设计中的应用过程,说明其如何支持面向对象的开发技术以及如何实现软件结构设计等问题,同时通过混合流水线制造系统实例开发出相应的仿真软件以说明UML的应用前景。     

用Sieve实现邮件过滤

Sieve是一种用来产生电子邮件过滤器的语言。为便于广大用户的使用,它设计得相当简单,但同时又内涵丰富,应用广泛。介绍了一种应用Sieve语言的电子邮件过滤系统。