Formalization and Verification of Business Process Modeling Based on UML and Petri Nets

In order to provide a quantitative analysis and verification method for activity diagrams based business process modeling, a formal definition of activity diagrams is introduced. And the basic requirements for activity diagrams based business process models are proposed. Furthermore, the standardized transformation technique between business process models and basic Petri nets is presented and the analysis method for the soundness and well-structured properties of business processes is introduced.

A UML profile for framework modeling

The current standard Unified Modeling Language(UML) could not model framework flexibility and extendibility adequately due to lack of appropriate constructs to distinguish framework hot-spots from kernel elements. A new UML profile that may customize UML for framework modeling was presented using the extension mechanisms of UML, providing a group of UML extensions to meet the needs of framework modeling. In this profile, the extended class diagrams and sequence diagrams were defined to straightforwardly identify the hot-spots and describe their instantiation restrictions. A transformation model based on design patterns was also put forward, such that the profile based framework design diagrams could be automatically mapped to the corresponding implementation diagrams. It was proved that the presented profile makes framework modeling more straightforwardly and therefore easier to understand and instantiate.

基于UMCS树的UML类图的混合相似性度量

软件重用是基于给定条件从存储库中检索以前开发的软件产品,检索基于相似性度量。UML(Unified Modeling Language)类图被广泛应用于软件设计,UML类图重用作为软件设计重用的核心而备受关注。因此,对UML类图的相似性开展研究。类图包含语义和结构信息。目前,UML类图的相似性研究主要集中在语义,也有个别讨论结构相似性,但没有考虑将语义和结构相结合。因此,提出一种结合语义和结构的混合相似性度量。鉴于UML类图的非形式化特征,将UML类图转换成图模型,搜索最大公共子图列表,构建了最大公共子图树,提出一个基于最大公共子图序列的混合相似性度量方法。针对概念公共子图和结构公共子图分别定义了语义匹配和结构匹配,并开展了相似性对比和基于相似性的分类质量比较实验,实验结果验证了所提出方法的优势。

带有并发行为的UML状态机图的形式语义

在软件开发过程中,UML(统一建模语言)状态机图是目前最流行的建模形式之一,它属于半形式化模型,无法用形式化的方法进行推理。为了能对UML状态机图进行推理,现有工作采用Petri网、时序逻辑语言XYZ/E、动态描述逻辑、Z(Object-Z)语言、CHAM化学抽象机等作为状态机图的形式语义,但这些语义都是行为语义,并没有从结构上直接形成体现真并发的形式语义。该文提出一种新的模型——统一结构模型作为带有并发行为的UML状态机图的形式语义,该模型不会增加或减少状态机图的任何信息。基于统一结构模型首先定义了状态机图的格局(全局状态),用于表现状态机图的执行过程,并且给出了UML状态机图的格局的转换规则,说明格局如何在状态机图中执行,在此基础上给出了状态机图的可达性算法,然后还对状态机图的死锁等性质进行了介绍,最后开发出一个原型工具,实现了状态机图的可达性分析,并用实例说明了该方法的应用。

MODELING OF FMS BASED ON UML AND OPNS

As the main component of computer integrated manufacturing system (CIMS), flexible manufacturing system (FMS) should be an open system with reusability and extenchaility. Moreover, as FMS is a complex asynchronous concurrent system, its model also should have the abilities to express the concurrency in the system and to analyze the behavior of the system. It is difficult to use any one method to model such a complex system as FMS. A modeling method using Object-oriented modeling language-unified modeling language (UML) and object-Oriented Petri nets (OPNs) is proposed. Class diagram in UML is used to represent the static relations among the objects in FMS. OPNs are used to model the dynamic behavior of the objects and conduct performance analysis. OPNs also can be used to identify the attributes and operations of the objects. The model can describe the system integrally and can be used to design FMS control software naturally.

Capability requirements modeling and verification based on fuzzy ontology

The capability requirements of the command, control, communication, computing, intelligence, surveillance, reconnaissance （C41SR） systems are full of uncertain and vague information, which makes it difficult to model the C41SR architecture. The paper presents an approach to modeling the capability requirements with the fuzzy unified modeling language （UML） and building domain ontologies with fuzzy description logic （DL）. The UML modeling constructs are extended according to the meta model of Depart- ment of Defense Architecture Framework to improve their domain applicability, the fuzzy modeling mechanism is introduced to model the fuzzy efficiency features of capabilities, and the capability requirement models are converted into ontologies formalized in fuzzy DL so that the model consistency and reasonability can be checked with a DL reasoning system. Finally, a case study of C41SR capability requirements model checking is provided to demonstrate the availability and applicability of the method.

A framework for an integrated unified modeling language

The unified modeling language(UML) is one of the most commonly used modeling languages in the software industry.It simplifies the complex process of design by providing a set of graphical notations,which helps express the objectoriented analysis and design of software projects.Although UML is applicable to different types of systems,domains,methods,and processes,it cannot express certain problem domain needs.Therefore,many extensions to UML have been proposed.In this paper,we propose a framework for integrating the UML extensions and then use the framework to propose an integrated unified modeling language-graphical(iUML-g) form.iUML-g integrates the existing UML extensions into one integrated form.This includes an integrated diagram for UML class,sequence,and use case diagrams.The proposed approach is evaluated using a case study.The proposed iUML-g is capable of modeling systems that use different domains.

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.

一种基于UML的智能导检系统设计方法

目的/意义探索建立带有智能导检功能的系统,为检验患者提供智能引导。方法/过程以检验科患者为调查对象,采用调查问卷获取并分析患者难点、痛点,利用Enterprise Architect软件、统一建模语言设计导检系统的用例图、时序图、部署图等,以测定尿微量蛋白肌酐比为例,设计智能导检系统知识库,依据评价问卷结果优化智能导检系统。结果/结论基于统一建模语言的智能导检系统设计方法可行,智能导检系统形式得到广泛认同,为推进结构化、智能化、知识化电子病历,提升医疗质量提供新思路。

Spatial data modeling for coalfield geological environment

Presented a study on the design and implementation of spatial data modelingand application in the spatial data organization and management of a coalfield geologicalenvironment database.Based on analysis of a number of existing data models and takinginto account the unique data structure and characteristic, methodology and key techniquesin the object-oriented spatial data modeling were proposed for the coalfield geological environment.The model building process was developed using object-oriented technologyand the Unified Modeling Language (UML) on the platform of ESRI geodatabase datamodels.A case study of spatial data modeling in UML was presented with successful implementationin the spatial database of the coalfield geological environment.The modelbuilding and implementation provided an effective way of representing the complexity andspecificity of coalfield geological environment spatial data and an integrated managementof spatial and property data.

UML到Event-B的系统化转换方法

在面向对象的软件开发中,UML已经成为事实上的建模标准。然而,UML虽然直观容易理解和应用,却存在着不精确的语义,而且UML是一种半形式化的建模语言,无法进行形式化的验证。Event-B是一种基于大量数学谓词逻辑的形式化方法,虽然精确却难以理解和应用。因此,如何结合UML图和Event-B方法的优点是研究的重点,以往的方法都是基于UML零散图到Event-B的转换,缺乏系统的转换方法。系统性的转换方法可以实现UML中的元素与Event-B中的元素相对应统一。一般的软件系统是中型系统,中型系统采用用例图、类图、状态图和顺序图这四种图就可以很好地表达清楚,有了上述的四种图,软件生命周期的需求获取、分析、设计、详细设计就可以完全表达清楚。文章中分别给出了这四种图到Event-B的转换方法,并将该系统的转换方法应用到对安全性和可靠性要求较高的电梯控制系统中。基于该实例的研究,验证了UML到Event-B系统性转换方法的可行性和有效性。UML到Event-B的系统转换方法不仅有利于UML的精确化和软件从业人员的使用,而且增强了形式化方法的可理解性,有利于形式化方法的推广和应用。

Modeling and OLAP Cubes for Database of Ground and Municipal Water Supply

Modeling plays an important role for the solution of the complex research problems. When the database became large and complex then it is necessary to create a unified model for getting the desired information in the minimum time and to implement the model in a better way. The present paper deals with the modeling for searching of the desired information from a large database by storing the data inside the three dimensional data cubes. A sample case study is considered as a real data related to the ground water and municipal water supply, which contains the data from the various localities of a city. For the demonstration purpose, a sample size is taken as nine but when it becomes very large for number of localities of different cities then it is necessary to store the data inside data cubes. A well known object-oriented Unified Modeling Language (UML) is used to create Unified class and state models. For verification purpose, sample queries are also performed and corresponding results are depicted.

An Embedded Software Modeling and Process by Using Aspect-Oriented Approach

In recent years, mobile devices have become widespread and refined, and they have offered increased convenience in human life. For these reasons, a variety of embedded systems have been designed. Therefore, improving methods for developing of embedded software systematically has become an important issue. Platform-based design is one example of an embedded-system design method that can reduce the design cost via improving a design’s abstraction level. However, platform-based design lacks precise definitions for platforms and design processes. This paper provides an approach that combines the aspects and platform-based design methods for developing embedded software. The approach is built on platform-based design methodology and uses the separating of concerns (SoC) concept to define the aspects and to reduce the crosscutting concerns in embedded system modeling. For aspect issues, we use the extended UML notation with aspects to describe both the static structure and the dynamic structure of the embedded system. We used an example of a digital photo frame system to demonstrate our approach.

基于UML活动图的用例识别

在面向对象的软件开发过程中,统一建模语言(unified modeling language, UML)的用例图用于捕获用户的需求.传统描述用例的方法一般是开发者根据自己的经验,从需求中人工获取用例.然而,如何自动生成准确的用例仍然是一个待解决的问题.本文提出了一种通过用UML活动图半自动生成用例的方法.首先通过引入形式化模型——统一结构来描述用例图与活动图,其次给出分解活动图的算法,然后根据分解活动图得到的依赖链生成对应的用例的事件流,从而得到用例模型,最后通过所开发的原型CASE工具进行案例的演示,验证了本文所提出的方法的可行性。

基于UML的企业内部办公流程计算机系统设计研究

如今,计算机办公系统的设计与应用已成为各行业加强办公管理智能化、提升办公经济效益的重要手段。在此,介绍企业内部办公流程计算机系统相关技术,分析计算机办公系统的需求,以统一建模语言(UML)为建模工具,对企业内部办公流程计算机系统进行整体设计和详细的各功能模块分析设计,包括办公流程发起功能设计、办公流程审批功能设计、流程跟踪查询功能设计以及通知公告功能设计,并经过应用测试,证实该计算机办公系统良好,满足各项内部办公流程功能需求,可在企业内部办公工作中投人使用,以期实现企业内部办公流程的有序化、规范化和流程化。

基于MBSE的作战能力跨域描述元建模方法

针对作战能力跨域描述存在语义二义性、不利于交流等问题,提出一种基于模型系统工程的元建模方法。抽象出作战能力元模型并给出形式化定义;从能力、作战和信息视角扩展作战能力元模型定义作战能力描述语言;通过UML Profile技术实现作战能力描述语言建模工具;借鉴面向对象分析方法思路提出作战能力描述语言建模方法。以美军“分布式防御”概念为例对提出方法进行实例验证。结果表明,提出的方法易于理解、可靠性和可扩展性强,有效消除语义二义性的同时满足多视角跨域描述作战能力的需求。

基于xUML与DODAF的指挥信息系统可执行体系结构建模研究

针对体系结构视图产品在验证系统动态行为及状态转换等方面存在的不足,难以有效保证所建模型与具体军事需求的一致性,提出了基于xUML与DODAF的可执行体系结构建模及验证方法,分析了该方法的可行性与适用性,及其在验证系统动态行为方面的优势,给出了利用该方法进行建模的具体步骤。最后结合区域防空指挥信息系统开发实例,通过建模对该系统的部分动态行为进行了验证和分析,进一步证明了该方法的有效性。

A Modeling Language Based on UML for Modeling Simulation Testing System of Avionic Software

With direct expression of individual application domain patterns and ideas,domain-specific modeling language（DSML） is more and more frequently used to build models instead of using a combination of one or more general constructs.Based on the profile mechanism of unified modeling language（UML） 2.2,a kind of DSML is presented to model simulation testing systems of avionic software（STSAS）.To define the syntax,semantics and notions of the DSML,the domain model of the STSAS from which we generalize the domain concepts and relationships among these concepts is given,and then,the domain model is mapped into a UML meta-model,named UML-STSAS profile.Assuming a flight control system（FCS） as system under test（SUT）,we design the relevant STSAS.The results indicate that extending UML to the simulation testing domain can effectively and precisely model STSAS.

面向业务自动化转型的铁路运输调度业务数据模型构建方法研究

铁路运输生产调度业务自动化、智能化转型改进是推动铁路运输效率提升的重要手段。探讨业务转型过程中对业务各场景各颗粒度控制逻辑和信息流通的梳理建模方法,从而推动业务高效转型,在对运输生产调度业务深入分析的基础上,抽象了调度业务组织的关键影响要素和关键关联关系,梳理了工作流、信息流、信息流通机制与上述抽象的调度业务要素及这些要素间关联关系的对应关系,设计了一种刻画业务工作流、信息流和信息流通机制的数据模型构建方法。考虑到铁路运输生产调度业务分散协作、多级耦合的多层级多场景特点,设计了工作流、信息流数据模型的分化、细化关联机制,以实现对不同层级、场景调度业务的数据模型间有机关系的刻画,最后结合实际调度业务进行了应用分析。结果表明该方法构建的数据模型可以规范调度业务在不同场景、不同颗粒度下的控制逻辑和信息流通,从而为业务自动化转型过程中的信息系统开发和作业流程再造提供参考。

UMLStatecharts的模型检验方法

统一建模语言UML已广泛应用于软件开发中,验证UML模型是否满足某些关键性质成为一个重要问题.提出了对UML Statecharts进行模型检验的方法.首先用扩展层次自动机结构化地表示UML Statecharts,然后给出其操作语义,通过寻找最大无冲突迁移集可以保证语义的正确性.对于具有无穷运行的系统,该操作语义可以映射到一个Bchi自动机.使用基于自动机理论的模型检验方法来验证UML Statecharts的线性时态逻辑性质,并给出方法验证由Statecharts和协同图建模的复杂多对象系统.