基于UML状态机与B方法的高可信嵌入式软件开发

提出了一套集成UML与B方法开发高可信嵌入式软件的实用方案:以软件的UML状态机模型为起点,将其转换为B抽象模型并在B工具中验证该模型的一致性,然后遵循B模型逐步精化的开发规则,利用B方法的精化正确性验证功能,得到系统的可靠的实现模型,最后借助B工具自动生成C代码。实例分析表明,这套方法可以提高高可信嵌入式软件的开发验证效率。给出了嵌入式软件设计中常用的UML并发状态图到B抽象模型的转换规则。

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

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

基于改进蚁群算法UML状态机图的测试用例生成

为了减少测试工作量,防止测试用例数目过多而导致爆炸,提出了使用改进的蚁群算法直接从UML状态机图中生成测试用例的方法。利用UML状态图是对系统可能的生命历程进行建模,由于状态图具有直观性,所以简化了生成测试用例过程,从而减少了测试的工作量。通过构造人工蚁群以及动态更新信息素矩阵,让蚂蚁选择还没有搜索或边信息素最小的顶点,确保了测试用例的数量既满足测试需求,又不会过多。通过编写算法及模拟仿真,对该算法的可行性和有效性做了验证和仿真分析。

UML状态机模型形式化验证技术研究

系统建模是系统开发经常用到的分析设计方法,如何保证模型的正确性一直是人们关注的话题。为了验证系统设计的模型正确性,进而提高整个系统的质量,提出了一种通过模型检查技术对UML状态机模型进行动态语义验证的方法。对状态机模型进行形式化描述,根据定义的映射规则将图形信息映射成模型检查器可以读取的语言,分析待验证的性质内容,通过使用模型检查器得到验证结果。

嵌入式系统内的UML状态机和框架技术分析

将UML状态机以及框架技术应用到嵌入式系统当中,不仅可以提高系统的开发效率,同时还可以确保系统运行的可靠性。与传统的有限状态机相比,UML状态机描述出来的嵌入式系统体现出了图形可视、逻辑通顺以及结构清晰等特征。本文以Quantum Platform框架为例,展开了嵌入式系统的相关应用分析。

UML状态机与框架技术在嵌入式系统中的应用

嵌入式系统中运用UML状态机和框架复用技术,在提高嵌入式系统开发效率、保证系统可靠性及系统可维护等方面有积极意义。相对于传统有限状态机,用UML状态机描述的嵌入式系统具有高度结构化、逻辑清晰、图形可视等特点。以基于Quantum Platform框架在嵌入式系统的应用为例,介绍了一种基于UML状态机的图形化建模开发和代码自动生成方法。该方法基于Quantum Platform框架以及相关开发组件,具有快速开发、方便调试、多平台移植、支持底层8位/16位低端单片机等特点。

基于UML实时状态图的定量分析

在实时系统的开发过程中,时间上的约束在系统早期的定量分析中起着非常重要的作用。UML作为一种图形化、面向对象的建模语言,其中的实时特性描述文件UML Profile for Schedulability,Performance and Time适用于对实时系统的刻画。在给定系统的实时状态图基础上,用相对应的随机Petri网模型进行定量分析,得到实时系统最终的分析结果,对系统开发有重要的指导意义。

飞机协同维修仿真的交互状态机模型

针对目前飞机维修场景众多的特点,提出一种适用于飞机协同维修的交互状态机模型。运用UML状态机建立维修人员、操作对象的状态转移模型,基于操作对象间的约束关系、操作对象-维修场景-维修人员的关系建立行为交互模型,将行为交互模型与状态转移模型融合,得到交互状态机模型,实现不同维修场景间的交互及状态变迁,给出模型的数学表达和图形化描述,使场景中实体对象的表达更加规范、统一,提高建模效率。以ADIRU排故为例,在分布式虚拟维修仿真平台上进行验证。

SPCE061A和μC/OS-Ⅱ平台的图形菜单研究

针对目前中低端嵌入式产品的需要,设计一种集图标、汉字混合显示的菜单组件,具有可扩展性、可移植性的特点;支持二值图像和GB2312编码汉字的显示。重点分析UML状态机的设计原理;详细介绍在凌阳SPCE061A单片机和μC/OS-Ⅱ平台上,这种菜单组件的软件实现方案,以及如何解决GB2312编码和图标存储的问题。

关于飞行模拟训练器电子仪表组件仿真模型研究

在模拟机电子仪表仿真中,针对仪表参数众多,且显示复杂的问题(参数随飞行状态改变),提出基于UML状态机和动态数据库相结合的建模方法建立仪表模型。利用UML状态机规范化仪表显示模型中元素的表达,增强了模型的可移植性。运用动态数据库建立仪表的消息分层传递机制,将动态信息流分层,实现仿真仪表上信息流的层次化表达。最后,以A320下ECAM显示的液压系统为例,对液压页面显示功能进行验证,表明该模型建立的合理性和有效性。

基于动作类的虚拟拆装过程运动建模仿真

针对装备拆装过程存在的拆装对象动作繁多,缺乏对各种零部件拆装动作的统一,不便于仿真实现的问题,提出维修拆装动作类对拆装运动进行描述,结合UML拆装执行基本拆装动作次数的不同,结合面向对象的思想提出了拆装动作类的概念,对拆装过程中具有相同动作次数的零部件做统一描述。利用UML建立拆装动作类的类图,结合状态机和拆装动作类建立拆装过程的运动模型。拆装仿真实例验证了动作类和拆装运动模型的可行性和实用性。

动态重组子网的Petri网飞机虚拟维修过程建模与仿真

针对大型民用飞机虚拟维修仿真中部件繁多、维修行为关系复杂、模型庞大等问题,提出可动态重组子网的Petri网飞机虚拟维修过程建模方法。使用UML状态机建立维修实体状态迁移元模型,以规范维修实体的维修行为,并将其转化为Petri网子网模型;依据部件间的联结关系构建双向邻接矩阵,约束各子网间的维修行为关系,进而建立可动态重组子网的虚拟维修过程模型。通过空客A320飞机交输活门作动筒组件的拆卸仿真实例验证了该模型的有效性。