基于Object-Z的带OCL约束的UML类图形式化描述

UML OCL是基于一阶谓词逻辑和集合论的形式化语言,用它对UML类图进行约束后类图便具备严格语法和精确语义,同时也具备了演绎验证的基本条件;但由于目前的建模工具还无法对缺乏精确语义的UML类图进行有效的演绎验证.因此提出了一种带OCL约束的UML类图通过Object-Z进行形式化描述的方法,这样便可以充分利用Object-Z强大的演绎验证能力来验证UML类图的正确性和是否具有某种性质等.     

采用模型检测器的软件安全模型验证方法

针对软件开发过程中安全性分析与设计不足的问题,在研究现有软件安全性建模及形式化验证技术的基础上,提出了一种适用于面向对象的软件安全性建模与验证方法.建立软件安全属性的非形式化UML模型,采用安全扩展有限自动机创建其形式化模型,并使用线性时序逻辑描述安全属性,将形式化模型与安全属性共同作为模型检测器的输入,得到模型是否满足性质的验证结果,从而实现了软件安全设计与验证技术的有机结合.实验结果表明,该方法能够在软件设计初期对所涉及的安全性进行有效分析与验证.     

基于时间自动机的UML模型转换与验证研究

针对无法对UML模型进行形式化验证的问题,提出在元模型层将UML模型转换为时间自动机模型并进行验证的方法.形式化UML状态机的结构,抽象出UML和时间自动机的元模型,利用模型转换语言ATL对UML元模型和时间自动机元模型构造映射规则,实现UML模型到时间自动机模型的转换,在模型验证工具Uppaal中对转换结果进行形式化验证.最后进行实例研究,结果表明了此方法的有效性和先进性.     

结合形式化方法的UML系统开发

介绍并讨论了在系统开发过程中使用UML(Unified Modeling Language)与其他形式化方法得到的一种精化模型，而且这一模型也同样支持形式化的分析和验证．     

一种验证Web应用设计的方法

提出一种表示Web应用的请求/响应导航关系的形式化行为模型,给出一种基于模型检查的Web应用设计的验证方法并描述了用时态逻辑CTL表示Web应用性质的方法.设计了一个检验方法可行性的原型框架,该原型嵌入自动化模型检查工具NuSMV,提供从UML设计模型到形式化模型的自动转换,在将用户输入的性质和形式化模型合并为NuSMV程序后,运行NuSMV进行自动化验证.     

UML类图元模型基于描述逻辑的表示及验证

UML类图元模型采用非形式化的表示,无法对其结构语义进行严格的描述,因此提出一种UML类图元模型基于描述逻辑表示及验证的方法.在对UML类图元模型进行分析的基础上,构建了UML类图元模型基于描述逻辑SHOIN(D)的约束规则集,并验证了UML类图元模型与其构建模型间的一致性.     

嵌入式实时软件建模方法研究

随着硬件设备计算能力的迅速提高以及社会需求的不断变化和增长,嵌入式实时软件变得越来越复杂.为了提高系统的安全性和可靠性,将基于UML的建模方法与形式化建模方法相结合,可以为嵌入式实时软件建模和验证提供一种良好的解决方案.采用UML扩展机制,在UML2.0顺序图中加入嵌入式实时软件建模所需的时间特性,并提出一种由UML2.0顺序图构造出时间自动机的方法,为下一步验证奠定理论基础.     

基于语义和结构的UML类图的检索

以软件重用为背景提出基于语义和结构的UML类图检索.构建了UML类图的重用模型,定义了存储UML类图的重用库结构.提出将本体的概念语义距离应用到UML类图的语义相似性度量和使用图表示UML类图的结构进行结构相似性度量.基于检索流程形式化检索需求,提出了UML类图的检索算法.基于提出的衡量标准,从语义、结构和混合三种检索类型对提出的算法进行了验证.实验结果表明,所提出的检索算法在检索质量和检索效率上要优于其他方法.     

UML 2.0的形式化语义研究

由于UML 2.0动态视图缺乏精确的语义,难以对它所表示的系统进行分析和验证.基于此,在描述UML 2.0顺序图和状态图语法和语法约束的基础上,采用可执行的线性时序逻辑语言XYZ/E定义其形式化语义,这样不仅便于UML 2.0顺序图和状态图之间的模型转换,也为使用UML和形式化方法相结合描述软件体系结构的交互行为奠定了基础.     

基于UML建模的电子病历系统设计与实现

以电子病历系统的开发为背景,介绍了UML在实际项目开发中的应用.在对电子病历系统进行需求分析的基础上,利用PowerDesigner对系统进行需求模型、静态模型和动态模型的建模,设计了基于UML用例图、类图和时序图的系统模型     

基于TCOZ的UML用例图的形式化模型

基于TCOZ,本文建立了UML视图的一种形式化模型,不仅为UML提供了一种精确的数学描述,也为其正确性分析和验证奠定了基础。     

Object-Z规格说明的结构模拟动画技术

形式化方法让软件需求的规格说明变得更加简洁精确,但是它的抽象难懂让用户难以确定形式规格说明中所叙述的用户需求就是他们所期望的.另外,大多的规格说明语言都是不可执行的,因此人们采用一种动画模拟的方式,将形式规格说明转换成一种可模拟执行的形式,从而帮助用户和规格说明者确认形式规格说明是否与用户的非形式化需求相一致.通过分析比较形式规格说明的两种动画策略———形式化程序合成和结构模拟的优缺点,决定使用结构模拟技术将Object-Z规格说明转换成SICStus Prolog可执行程序并加以执行,从而实现对Object-Z规格说明的确认.     

UML在管理信息系统中的应用

UML是一种定义良好、易于表达、功能强大且普遍适用的建模语言.它溶入了软件工程领域的新思想、新方法和新技术.它的作用域不限于支持面向对象的分析与设计,还支持从需求分析开始的软件开发的全过程.介绍了UML的主要内容、主要特点及应用领域,以一个城镇地籍管理信息系统为例,阐述了UML在开发管理信息系统中的应用.     

一种基于Object-Z的面向方面建模方法

提出一种基于Object-Z的形式化面向方面建模语言及其建模方法。方面规范提供了观察基本模块和方面模块的行为、描述它们相互关系的手段,编织机制将两类模块系统地集成为一个完整的系统模型。该方法能有效地简化系统建模,提高系统模型的可复用性,也为进一步验证系统性质提供了理论基础。     

基于接口的构件建模方法

软件复用是当前软件开发研究的一个重要领域，基于构件的软件开发方法是复用研究的重点。但是传统的软件设计技术不能很好的满足基于构件的系统的需要。它们对于基于构件的系统的设计只提供了很少的技术和指导。本文提出一种基于接口的构件建模和设计方法。这种方法使用UML作为工具，提供了系统化的构件建模手段。     

基于UML软件开发过程的CASE平台研制

针对基于UML的面向对象软件开发支持环境CASE平台的研制,给出了平台的需求定位和实现目标,讨论了平台组织的总体方案和功能,并据此给出了平台体系结构的设计和实现方案,阐述了平台设计和实现中的模型建立、数据存储机制实现方案,较成功地用于基于UML软件开发过程的CASE平台。     

家庭自动化系统中的建模设计

该文以家庭自动化系统为背景,探讨了利用统一建模语言进行面向对象的建模问题,介绍了UML的结构和机制,说明如何在软件开发过程中运用UML建模.按照此模型进行系统的开发,可以大大地提高系统开发的产业化水平,是软件工程的一个发展方向.     

基于UML的软件结构规范与精化

提出利用UML表示软件体系结构不同的视,表明了UML可以用于建模软件结构。UML的图形语义用通信顺序进程CSP的符号表示,进一步,基于CSP的语义可以链接不同的软件结构模型。还讨论了软件结构规范的精化问题,该精化过程可以保留系统需要的属性。     

Rigorous Modeling of Real-time System Based on UML and PVS

Rigorous modeling could improve the correctness and reduce cost in embedded real-time system development for models could be verified. Tools are needed for rigorous modeling of embedded real-time system. UML is an industrial standard modeling language which provides a powerful expressi-veness, intuitive and easy to use interface to model. UML is widely accepted by software developer. However, for lack of precisely defined semantics, especially on the dynamic diagrams, UML model is hard to be verified. PVS is a general formal method which provides a high-order logic specification language and integrated with model checking and theorem proving tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time system. In this approach, we provide 1) a timed extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexible and friendly in modeling, extendable in formalization and verification content, and better performance. Time constraints are modeled and verified and its a highlight of this paper.