一种从UML类图和协作图到状态图的转换方法

统一建模语言(unified modeling language,UML)状态图是基于UML开发的软件设计模型的重要组成部分,它描述了一个对象所处的可能状态以及状态之间的转换。对一种生成状态图的方法进行了改进,以类图和协作图为基础,创建单个对象的状态图,对系统中单个对象的状态图进行集成生成整个系统的状态图。结果表明,生成的状态图具有较高的结构化和可读性。     

业务过程建模及其形式化验证

针对业务过程建模复杂、模型一致性难以保证的问题,提出一种求精式业务过程建模及其形式化验证方法.结合语义本体技术、基于统一建模语言(UML)的扩展机制,实现对业务过程中的不同关注点进行多视角地可视化建模.业务过程建模是一个“整体抽象过程→声明式过程→命令式过程”多阶段的求精过程.引入环境本体的概念,以软件交互对环境状态的影响来描述软件行为和能力,并在此基础上给出了模型相关定义及其形式化语义.结合一个简化的产品交易系统实例详细论述如何采用声明式形式化语言Alloy进行业务过程模型定义和模型求精的形式化验证.实例表明,采用分阶段求精式业务过程建模方法,并围绕模型语义通过Alloy语言进行形式化验证,可以有效地提升建模过程的灵活性和保证模型规范的一致性.     

基于PVS的飞机订票系统的形式化描述与验证

形式化方法主要应用于安全性第一的系统的规范与形式验证。原型证明系统PVS为开发和分析形式化规范和验证提供了一个集成化环境。本文介绍PVS系统的证明方法和特点 ,并利用PVS系统对飞机订票系统的需求给出了形式化规范 ,对部分关键属性完成了证明 ,说明了使用PVS系统的某些经验和技巧     

一种UML状态图模型检测方法

为在开发过程早期发现系统设计的各种错误与不一致,提出一种UML状态图模型检测方法,用于验证设计模型与需求规约间的一致性.该方法通过元组定义UML状态图的主要元素,给出状态图的中间表示形式SC.基于SC上定义的操作语义,该方法将状态图转换为具有KRIPKE语义结构的状态迁移系统,并将系统需满足的性质表示为线性时序逻辑公式...     

基于时间自动机网的C3I系统建模和实时性验证

针对目前缺乏描述和分析C3I系统的理论基础,提出了基于时间自动机理论的C3I系统的数学模型.建立了C3I系统中各个子系统的时间自动机模型,子系统之间通过通道进行通讯,通过时间自动机网把C3I系统构建为多个并行的时间自动机的网络模型.提出基于计算树逻辑CTL的C3I系统的实时性表达方法,详细描述使用模型检测工具Uppaal对C3I系统建模和所建模型的实时性验证的方法.实验结果证明,基于时间自动机的C3I系统的建模与模型检测方法是有效的,为C3I系统行为的分析、验证提供理论基础.与经典算法相比,该方法提高了对C3I系统建模和分析的效率.     

安全协议UML模型的SPIN分析

统一建模语言(UML)是设计和建模安全协议的常用方法,但UML缺少精确的语义,不能对协议模型作进一步分析和验证;Promela是一种具有精确语义的形式化语言,通过Promela规范给协议的UML模型赋予精确语义可以结合两者的优势,提出一种将安全协议UML模型转换成Promela规范的方法,定义了     

MSVL程序的自动定理证明方法

The MSVL is a temporal logic programming language. It can be used to verify C, Verilog/VHDL programs. To do so, a program written in C or Verilog/VHDL is translated to an MSVL program, and then the task is changed to verify MSVL programs. However, at present, the correctness of MSVL programs can only be proved by hand with deductive approaches. This is tedious and error-prone. To handle this problem, an automatic theorem proving technique for the MSVL based on the interactive theorem prover PVS is proposed. To this end, first the syntax and semantics of the MSVL are described in the specification language of PVS, which enables MSVL programs to be correctly recognized by PVS. Further, an axiomatic system of the MSVL and some theorems are specified. Then the proof commands of PVS are input for invoking the PVS prover to deduce MSVL programs. During verification, simple details can be proved by PVS automatically while complex steps are controlled by human. In this way, MSVL programs can be verified semi-automatically, which facilitates the deduction of MSVL programs. An instance of the bakery algorithm is given to show that our method is feasible.     

模型检测与定理证明相结合开发并验证高可信嵌入式软件

首先将软件的UML状态机模型转换为模型检测工具MOCHA的输入语言REACTIVEMODULES,在MOCHA中进行正确性验证,利用模型检测工具针对错误情况给出的反例路径,尽早修改软件的UML设计模型;然后将已验证过的UML模型转换为定理证明工具B方法的抽象规约,利用B方法的精化、验证及代码生成功能,直接生成正确的C代码。并给出了从UML状态机到REACTIVE MODULES建模语言及B AMN抽象规约的转换规则。实验结果表明,该方法可在软件工程中有效地提高高可信嵌入式软件开发和验证的效率。     

基于安全协议操作语义模型的组合协议分析及验证

协议的可组合性问题是安全协议形式化分析及验证领域的一个公开问题,通过提出采用安全协议的操作语义模型对组合协议进行形式分析和验证,建立了Yahalom和Denning-Sacco组合协议的操作语义模型,并用基于操作语义模型的自动化验证工具Scyther验证了其安全性,发现了一个针对Yahalom协议机密性的组合攻击.结果表明,操作语义模型是分析与验证组合协议的一种可行方法.     

基于UML活动图的动态工作流过程建模的研究

在形式语义的支持下,提出了一种适合动态工作流过程建模的方法.该方法在扩展UML活动图的基础上给出了一种建模机制,利用扩展的UML活动图来对动态工作流的过程进行建模.最后,将该方法用于一个汽车企业产品研发的过程建模实例,且建模结果证明该方法是适合的.说明了基于扩展的UML活动图的工作流过程建模方法对动态工作流过程建模的有效性.     

面向信息物理融合系统的异构模型转换方法

作为一种深度网络化嵌入式系统,信息物理融合系统(Cyber-Physical System,CPS)具有联合动态性、系统组成异质性、计算过程与物理过程的多尺度融合性等典型特征,使得基于单一模型的传统嵌入式系统模型构建和仿真验证方法面临新的挑战.在CPS系统设计开发与仿真验证时,往往需要组合使用多种设计模型或建模语言以描述信息域与物理域实体特点.针对CPS计算物理深度融合的问题,在分析基于计算模型和物理模型进行CPS系统协同开发需求和可行性的基础上,以统一建模语言(Unified Modeling Language,UML)模型和仿真(Simulink)模型分别作为计算过程和物理过程典型建模方式,研究了连续时间和离散事件模型间的结构映射和行为映射,提出了一种Simulink模型与UML类图和活动图之间的转换方法,并通过ATL(ATLAS Transformation Language)转换规则实现了技术验证.     

基于场景的并发系统需求验证方法研究

为验证并发系统需求设计的正确性,提出一种基于场景的并发系统需求验证方法.首先,用UML顺序图建模并发系统需求场景,通过定义顺序图的操作语义及转换规则,将顺序图的XML描述文件自动转换为Promela程序,而后将描述系统需求的Promela程序和描述系统规约的线性时序逻辑作为模型检测器SPIN的输入,用模型检测的方法自动...     

基于稠密时间的实时系统模型检测的一个应用

模型检测是一种用于并发系统性质验证的算法技术。实际生活中广泛应用的是带有时间约束的并发系统即实时系统，现在模型检测技术越来越被广泛地应用到这类系统的性质验证当中。这类系统通常用时间自动机来表示，而它们的性质则用时序逻辑公式表示。本文简要介绍了时间自动机和时序逻辑TCTL，并着重说明了如何进行基于稠密时间的实时系统的模型检测，最后给出了一个应用实例。     

一种结合UML和B的软件需求获取方法

精确的软件需求是软件质量的保证,UML在软件需求中起着重要的作用,它用于描述软件的需求模型、对象模型、动态模型和部署模型.然而UML缺乏形式化方法的准确语义,很难产生准确无歧义的软件规约.使用B和UML结合的方法,借助形式化方法的精确语义和规约级证明义务来产生准确一致的系统规约,并结合家庭智能控制系统说明了结合使用B和UML规约的过程.     

A unified linear-time temporal logic solution to the steam-boiler control specification problem

The TLL XYZ/E is a formal language able to represent the dynamic semantics and the static semantics in a unified framework. It supports the whole process of program development, i.e. from the abstract specification to the efficiently executable program in a formal, precise and convenient way. The steam boiler control specification problem, a large case study in the fields of real time, hybrid and communication systems, is discussed with XYZ/E. The approach covers physical model construction, formal specification, stepwise refinement, verification, executable program and visual user interface programming.     

基于符号模型检验的可信跨域协作系统验证方法

针对规范调控的可信跨域协作系统属性验证的困难,提出一种基于符号模型检验的可信跨越协作系统验证方案.该方案包括规范语法及其状态语义、系统抽象模型、验证算法三大部分.其中规范的状态语义是方案的核心,它将规范集映射为其所对应的状态或状态转移集,消除了系统模型和规范的语义不一致性;系统抽象模型包括规范Kripke结构和路径规范性定义,以及规范Kripke结构的分支时态逻辑（CTL）语义3个部分,实现了可信系统的形式建模;验证算法描述了系统符号模型检验的具体实现过程.与基于定理证明的验证方案相比,该方案有效降低了验证时间,提高了验证效率.     

结合硬件特征的UML建模方法在嵌入式系统中的应用

为了解决UML对硬件特征描述较弱,软硬件设计时关系不紧密的问题,本文提出了结合硬件特征的UML建模方法。该方法将实时性、精度、环境要求等特性在模型中进行体现,同时将模型和开发流程有机的结合起来,不但提高系统设计的质量,也能针对不同需求快速修改设计。     

基于CPN的UML2.0形式化建模

UML作为一种半形式化建模语言,很难对系统进行动态的仿真与性能评价。基于着色Petri网（CPN）拥有严格的数学理论基础,能够对系统进行图形化的模拟与分析,提出了一种UML的形式化建模方法。对UML2.0顺序图中opt等操作符给出了对应CPN图形的转化规则,实现了用CPN模型描述UML2.0的用例图与顺序图的目的。以一个简单的UML2.0顺序图进行验证,结果表明所提方法是有效的。     

基于改进随机状态图的制造系统建模

为减少应用随机状态图进行制造系统建模的复杂性,引入抽象子系统和系统总图,分别表达随机状态图的相似性和整体性．应用改进后随机状态图建立了制造系统模型,将该模型转化为时间连续马尔可夫链,并对系统的性能指标进行了分析．实例验证表明,改进随机状态图能有效简化建模与性能分析过程,为制造系统设计与优化提供依据．     

基于Uppaal的移动IPv6协议的模型检测

采用形式化方法对移动IPv6协议系统建立了时间自动机模型,使用实时模型检测工具Uppaal对所建模型的关键性质：活性、移动性和平滑切换等进行了分析和检测. 检测结果证明,移动IPv6协议在切换时存在丢包现象. 通过分析丢包产生的原因,提出了移动IPv6实现平滑切换的理想时间约束条件,并在理想条件下重新验证了协议的性质. 结合模型在理想约束条件下的检测结果指出了提高移动IPv6移动性能的设想.