面向模型检验的UML状态机语义

UML状态机(SM)是UML中用来对系统各种元素的离散行为建模的图.它丰富的表示符号提供了强大的描述机制,但也降低了其结构的模块性,提高了对其分析验证的难度.模型检验是自动检验有限状态并发系统的技术.通过模型检验SM描述的不同系统元素的行为是否满足某些性质,能尽早发现设计中的错误.为了将模型检验技术应用于SM的验证,本文用kripke结构定义SM的操作语义.与已有的SM语义定义不同,本文考虑到了SM中包含的不确定因素,用kripke结构描述系统所有可能的演化轨迹.通过检验从SM翻译得到的kripke结构达到模型检验SM的目的.     

UML Statecharts的切片模型检验方法

统一建模语言UML已被广泛应用于软件设计和开发中，而验证UML模型是否满足关键的性质需求成为一个重要问题。由于空间爆炸和语义的复杂性，对Statecharts进行模型检验受到软件规模和设计精化程度的制约。本文在用扩展层次自动机（EHA）结构化的表示UML Statecharts后，通过分析EHA中存在的层次、并发和事件同步等特征定义了一组依赖关系。对于由状态和迁移组成的切片准则，给出对EHA进行切片的算法。该算法能保证切片后的EHA与原来的Statecharts对性质具有相同的可满足性，且删除了与被验证性质无关的层次和并发状态，缓解了空间爆炸问题。     

UML Statecharts的切片模型检验方法

统一建模语言UML已被广泛应用于软件设计和开发中,而验证UML模型是否满足关键的性质需求成为一个重要问题.由于空间爆炸和语义的复杂性,对Statecharts进行模型检验受到软件规模和设计精化程度的制约.本文在用扩展层次自动机(EHA)结构化的表示UML Statecharts后,通过分析EHA中存在的层次、并发和事件同步等特征定义了一组依赖关系.对于由状态和迁移组成的切片准则,给出对EHA进行切片的算法.该算法能保证切片后的EHA与原来的Statecharts对性质具有相同的可满足性,且删除了与被验证性质无关的层次和并发状态,缓解了空间爆炸问题.     

基于UML的建模及模型检验研究

UML是一种广泛使用的面向对象的可视化统一建模语言,但UML缺乏精确的语义描述,难以对UUL模型进行分析验证以判断设计规范是否满足目标需求。符号模型检验是一种能够有效保证系统可信性质的自动检验技术。为了检验UML模型的正确性,在建模的基础上把UML模型转换为SMV模型,然后使用符号模型检验器（SMV）对模型进行检验,有利于在系统的设计早期发现系统的缺陷。     

UML状态机到B形式化规约的转换

文章研究在高可信软件工程中集成形式化方法。以软件设计的UML状态机模型为起点．将其转换为B形式化模型，然后在B工具环境中遵循B方法的精化原则和正确性验证方法，开发出可靠的实现模型。提出一套从UML状态机到B形式化规约的转换规则，涵盖UML基本状态图、分层状态图和并发状态图。实例分析表明．这套转换规则行之有效。     

GSM中基于状态机模型的HLR操作实体

基于对某种ＧＳＭ移动程控交换机归属位置寄存器ＨＬＲＭＡＰ Ｕｓｅｒ操作实体的工作原理,对ＨＬＲＭＡＰ Ｕｓｅｒ操作实体中各业务处理流程进行详细分析,考虑到各种业务处理的并发性,采用有限状态机的设计思想,对各业务处理过程进行管理调度,按照消息驱动状态转移的原则,记录每个过程标识ＩＤ及其当前状态,过程处理中状态数据包完整记录了线索信息,保证了状态的正常演进,对于数据的冲撞采用了消息缓存机制,并且保证了过程的有序进行。这种基于有限状态机模型的设计方案适合于实时、并发系统的设计。     

面向工程化教育的有限状态机教学设计

有限状态机是"硬件描述语言"课程教学的重点和难点。本文深入分析当前有限状态机教学的现状,指出有限状态机教学与工程化人才培养需求的之间差距。在此基础上,论文提出并阐述了一种问题驱动的有限状态机教学体系,对算法状态机图和模板式编码风格等有限状态机设计的相关概念和方法进行了阐述。     

模态逻辑S4的覆盖语义及其完备性

 基于第六种覆盖粗糙集模型提出了模态逻辑S4的覆盖语义,利用覆盖模型与Kripke模型之间的关系,证明了覆盖语义的可靠性和完备性定理.进一步讨论了覆盖语义与Alexandrov拓扑语义之间的关系.证明了覆盖语义与Alexandrov拓扑语义是和谐一致的.     

基于符号模型检验的硬件验证

随着程序或电路规模的增大，状态数目将呈指数增加而引起组合爆炸。符号模型检验是形式化方法的一个重要方面，可以处理大规模的数据和控制序列，缓和了组合爆炸的问题。文章介绍了符号模型检验的原理和方法，利用验证工具VIS验证了8位微处理器PIC的一些关键属性，并给出实验结果。     

UML技术在医院检验信息管理系统设计中的应用

目的:针对医院对检验信息管理系统的开发质量要求,研制解决方案,避免后期投入成本巨大浪费问题,实现因地制宜地保证系统上线。方法:采用标准的UML方法,编制了适合医院的检验管理信息系统,并完成了详细描述了其具体用例图(Use Case)、顺序图(Sequence Diagram)、类图(Class Diagram)。结果:设备的开机率提高了20%,标本控制时间明显缩短,故障响应时间为1分钟,在系统中及时报警提示。结论:完成了基于UML的LIS系统的设计,提高了设备的工作效能,收到了良好的效果。     

基于模型检测的UML状态图和顺序图一致性检测

用户可使用UML从不同角度对系统进行建模,但不同视图间存在信息冗余,会导致视图不一致的问题。文中提出形式化与可视化UML互补建模的方法,探讨用模型检测验证UML模型中的状态图和顺序图的一致性问题。针对具有复合片段的顺序图提出分析方法,将复杂层次结构的状态图转换为有限状态机,再用模型检测工具NuSMV对建立的模型进行验证。最后通过实例对此转换方法进行验证,实验结果表明了此方法的有效性。     

一个面向方面的UML扩展

本文给出了一个面向方面的UML扩展,描述了扩展的构造型及其含义。对于面向方面程序设计中的核心元素,给出了相应的元模型。该UML扩展为面向方面建模提供了一种可行的方法。     

基于相似性计算的领域模型语义查询

为提高领域资产库的复用能力,解决领域模型与用户的个性化需求不能完全匹配时仍能为目标应用系统的构建提供支持的问题,提出了领域模型语义查询算法.通过服务模型相似度计算结果,建立同一问题域中同类模型之间的语义关联,并以此为基础,提出领域模型的语义查询算法.最后介绍了该算法在领域建模平台中的应用.     

基于MDA的语义Web服务的组合与验证

针对语义组合Web服务的验证问题,研究了模型验证相关技术、统一模型语言(UML),提出了基于模型驱动架构(MDA)的组合方法.该方法使用UML类图和用例图对OWL-S进行静态组合建模,使用活动图对OWL-S进行动态组合建模,实现了语义组合Web服务的UML描述,然后将该描述转换为Promela语言代码,在Promela代码之后增加LTL的声明,使用SPIN工具进行正确性、安全性和活性验证.该模型保证了组合过程的正确性.     

UML中衍型的精确定义与分析

UML规范对于衍型这种扩展机制描述的不够清晰和严格，常被用户和研究者误用，并且也无法很好地支持可扩展的建模工具的开发．本文精确地定义UML中的衍型以及衍型之间的关系，在此基础上定义衍型与元模型之间的转化并提出运用衍型的指导规则，使得UML衍型的使用者能够更深入地理解这种扩展机制，并为支持衍型的建模工具的开发提供可靠的理论基础．     

基于UML的嵌入式系统模型验证技术的研究

统一建模语言UML在嵌入式系统设计建模中已经获得了广泛的认可,能对复杂嵌入式系统建模,并有很多成功的应用,但UML是一种半形式化语言,存在时间约束描述能力不强和所建模型形式化复杂、验证难度大等问题。针对上述问题,本文提出了采用实时UML对嵌入式系统UML状态图进行建模;然后用状态-约束-事件矩阵方法来对模型进行形式化描述;最后利用SPIN对模型进行验证。该方法解决了UML在嵌入式系统建模和形式化验证过程中出现的问题,应用实例和结果证明了该方法的有效性和可行性。     

面向语义通信的语义知识库综述

语义知识库是一种可为数据信息提供相关语义知识描述的、结构化的且具备记忆能力的知识网络模型，是语义通信的关键使能技术之一。首先，归纳分析计算机领域语义知识库研究现状，说明知识库在语义信息提取等方面的关键作用；然后，梳理无线通信领域中信源、信道、任务语义知识库的研究现状，揭示语义知识库在语义传输效率提升方面的潜能；最后，分别从多层级构建、动态智能演进、多智能体协同更新3个方面分析了语义传输中语义知识库面临的挑战。对于如何深度融合人工智能与通信技术，创新性地提出多层级语义知识库框架，认为一个跨模态、跨任务、跨环境的知识库的构建是高效语义传输的重点研究方向。     

面向6G的语义通信

6G移动通信的高可靠、高频谱效率传输需求对于经典信息论指导下的传统通信技术构成了挑战,提取信源语义特征进行编码传输的语义通信技术,为6G移动通信提供了新型解决方案.首先简述了语义信息论基本观点,探讨了语义信息的度量——语义熵,然后提出了语义通信的系统框架,针对文本与图像信源,分别设计了语义编码方案,并与传统编码方案进行...     

基于有限状态机的雷达状态模型建立

现代雷达具有功能多特点.针对雷达系统控制,采用传统程序设计方法存在调试周期长,可移植性和可扩展性差的特点.本文采用有限状态机理论对雷达状态进行模型建立,根据状态机理论,通过仿真建立相应的状态切换模型,工程实践表明有限状态机能较好的进行雷达系统控制设计,系统可扩展性、可移植性较好.     

基于有限状态机的联锁平台任务同步模型研究

二乘二取二铁路计算机联锁系统中,两套4个CPU组成了容错计算结构,实现CPU之间的同步是基于表决的容错计算机系统的关键过程。因此,本文提出了一种基于有限状态机的主/备/从并行任务同步模型,用于准确描述系统中不同CPU对象的任务同步状态,为二乘二取二同步通信表决过程大规模复杂的逻辑和时序设计提供了方法学上的参考和简化。