分区操作系统内核中隔离性质的研究

为了达到经过形式化验证分区操作系统内核隔离性质的目标,采取形式化方法描述系统的顶层规范设计中描述隔离性质需求,通过将航空电子应用软件标准接口ARINC653与GWV定理相结合,实现了对分区操作系统需要满足的隔离性质的抽象描述,并通过使用类Z/Z++作为形式化描述语言。     

面向VLIW DSP处理器的智能汇编过程语法处理方案

近年来高性能数字信号处理器(DSP)得到快速发展.高性能数字信号处理器处理任务所需的时间和能耗与对代码的指令级并行度的挖掘密切相关.为了获得高指令级并行度的代码,提高代码的可移植性,同时减轻软件开发人员的负担和减小编程的难度,我们提出了智能汇编这种抽象汇编程序解决方案来综合了高级语言和汇编语言两方面的优势.针对这种抽象汇编程序,需要智能汇编器这种面向高性能VLIW DSP硬件底层的优化编译器.智能汇编器是基于抽象的智能汇编过程进行代码优化的.本文提出了一种考虑高性能VLIW DSP硬件特性的智能汇编过程结构,并介绍了对这种智能汇编过程进行语法处理的方案和相应的核心算法以对这种过程和过程中的指令序列进行识别,能够为后续的代码优化环节提供过程和指令的语法信息.     

一种Verilog的操作语义

用形式化的方法描述了硬件描述语言Verilog的语法和语义,建立了一个Verilog的操作语义模型。分别用二元组和四元组描述Verilog非并发和并发成分的状态,刻画了不同语句的状态转换规则,并用实例描述了并发程序的执行过程,证明了该操作语义模型的正确性。     

利用扩展的Petri网模型形式化业务场景模型

UCM模型作为一种图形化的业务场景模型,其场景设计可以表示需求和产生规格,驱动设计和系统演化,UCM模型的正确性影响软件开发的质量.鉴于形式化模型可以验证其正确性,提出了一种利用扩展的Petri网模型,应用模型驱动实现业务场景模型的形式化方法.该方法通过细化Petri网模型中的Transition结点,从而有效的描述业务场景模型中的路径决策和动态行为.通过对UCM模型和扩展的Petri网模型的抽象语法定义,利用模型驱动方法定义了UCM模型元素形式化映射为Petri网模型元素的规则,并根据其规则设计了映射算法;在Eclipse平台上使用ATL语言实现了模型的形式化映射;应用Web Payment实例演示了UCM模型的形式化分析结果.     

面向芯片的嵌入式实时操作系统设计模型

传统嵌入式实时操作系统的设计采用一体化、高效大内核结构的方法,在可伸缩性、可移植性和对新型结构的硬件平台的支持以及接口标准的开放性方面较差．在对实时操作系统（RTOS）分析的基础上,提出了一种面向芯片的嵌入式实时多任务操作系统的设计模型．对硬件抽象层和操作系统内核的构造进行了研究,再对ERTOS的可伸缩性、实时性、可移植性以及应用编程接口设计进行了详述．该设计模型引入硬件板级支持软件包（BSP）来支持操作系统在各类OEM板或用户定制硬件系统板上的移植,从而解决了传统系统的缺陷,满足了当前对ERTOS的需求．     

基于CPU仿真器的汇编语言学习系统设计与实现

提出一种基于CPU仿真器的汇编语言学习系统设计模型和实现方法.该系统利用JavaBean组件技术实现CPU的仿真;结合多线程技术和锁机制实现组件的数据触发式调度机制,有效地解决了具有复杂关系的组件之间的调度运行问题,保证了微命令的有序执行;基于脉冲信号的事件触发机制,实现了微指令的单步调试;基于所设计的CPU仿真器指令系统,采用现代编译技术设计了一种汇编器,实现了CPU仿真器上汇编指令到机器指令的快速编译.与已有的汇编语言学习系统相比,本系统不仅在通用性、交互性等方面都有较大提高,而且能形象直观地展示虚拟寄存器等各个虚拟芯片的实时状态,记录对应的微指令流,从而更精确地监视汇编指令在CPU仿真器中的执行过程.     

基于构件的服务模型形式化语义描述

为解决服务系统描述和构建过程中服务的组合和验证等方面的问题,以范畴理论为基础,引入进程代数,为服务系统的架构模型提出了一种形式化的语义描述方法.整个服务结构模型通过由服务标志和标志态射构成的范畴图表来描述,态射用来表示服务规范之间的关系,余极限用来描述服务的层次组合.以此为基础,进一步从服务端口、结构和行为等方面对服务的组合、分解以及精化过程所中应保持的语义特性进行了分析.实例研究表明:该框架不仅能在抽象层次上支持服务系统的建模和分析,而且还可通过映射抽象模型到实现技术来支持服务组合,可以很好地分析需求分解和服务组合的正确性,可用于指导服务系统的描述和构建.     

基于Petri网的保险工作流系统建模及验证

提出基于Petri网的工作流系统业务模型.该模型将Petri网的理论和性质应用于业务工作流系统当中,从系统的运行过程和形式化的图形描述方式两方面实现对工作流系统的快速建模和分析.通过工作流Petri网的语义性质,对所建立的中国人民保险公司的索赔业务工作流系统模型的正确性进行验证和分析,表明此模型有较好的应用效果.     

Biba实用模型的自动化形式验证

通过给传统的Biba模型增加相应的敏感级函数,完善其主客体完整性标签,并对其安全操作规则进行相应的改进,使其适应实际的应用需求.采用完全形式化的方法对改进后模型中的各元素、模型必须满足的不变式以及模型迁移规则进行描述,并在此基础上利用定理证明器Isabelle完成对该模型的自动化形式验证,从而实现高等级安全操作系统研发过程中对安全策略模型的形式化需求.     

基于超图文法的软件体系结构动态演化

提出用带约束的超图表示软件体系结构,给出基于超图态射的软件体系结构动态演化通用产生式规则的形式化语义和操作,定义类型超图作为体系结构风格,运用超图文法和体系结构风格建模软件体系结构动态演化.为了验证软件体系结构动态演化的正确性,采用模型检测技术,设计算法对软件体系结构动态演化性质进行形式化验证,并应用模型检测工具进行实验分析.该方法既提供了图形化的直观表示,又展示了基于文法的形式化理论框架.     

基于UML需求建模的一种形式化分析方法及其应用

UML是软件开发过程中广泛使用的建模语言,但由于缺乏精确的语义,难以直接对其建立的需求模型进行精化和验证,因而无法进一步提高软件的正确性和可靠性,也不具备实现软件自动化的前提条件.提出了一种基于UML需求建模进行形式化分析的方法.采用Object-Z对UML建立的需求模型进行形式化描述,采用Perfect弥补了Object-Z在精化与验证方面缺少自动化工具支持的不足,最后通过一个实例说明了该方法在实际应用中的可行性.     

基于本体的多无人机系统语义互操作方法

引入基于领域本体的语义模型形式化建模方法,提出了多无人机交互描述的语义描述模型方法和交互配置的语义增强方法.设计了无人机本体UAV O和服务描述本体UAV OS,在OWL S（Ontology Web Language for Services）基础上扩展服务动态特性等的描述,可以为服务质量、服务状态和服务关系提供语义描述;扩展了对多无人机任务和动态配置、组合所需控制结构等的描述.为了实现多无人机应用配置的自动化和动态性,基于本体的语义增强方法可以用于配置管理,在匹配中引入高层次的语义增强匹配,对多无人机交互配置处理进行语义增强.在无人机综合仿真环境中进行了验证,结果表明,提出的基于本体的语义互操作方法能有效地支持多无人机应用交互和集成.     

基2的流水式快速傅里叶变换处理机的形式化模型

快速傅里叶变换(FFT)的应用领域非常广泛,其硬件实现方法多种多样。传统的电路正确性验证的方法是模拟,这种方法的主要缺点是不能穷尽模拟全部输入情况,而形式化方法使用纯数学手段证明电路具有某些属性,从而证明其正确性。所以用形式化方法验证FFT电路的正确性具有极强的实用价值。形式化验证的第一步工作是对要验证的电路进行建模,因此本文首先介绍了国内外FFT形式化建模的主要方法和优缺点,然后用重写系统给出了任意N=2M点的基2的流水式快速傅里叶变换处理机的形式化模型,显示了重写系统用于复杂硬件电路建模的优越性,为进一步的电路正确性验证奠定基础。     

用于C语言程序验证的性质描述语言C-PDL

为了保证程序的正确性,可以先将程序抽象成模型,再采用模型检测技术对模型进行验证.模型检测工具只接受形式化的性质描述语言,而一般程序员很难正确地使用,因此,文章提出了半形式化的描述语言C-PDL,并介绍了采用C-PDL描述性质的验证系统.C-PDL采用时序逻辑语言XYZ/AE的语法结构,结合了C语言程序性质的特点,引入规范模式系统,其语法简单且描述能力强.另外,C-PDL表达式可以方便地转换成模型检测工具识别的各种时序逻辑公式.     

基于B方法的内存管理模型的设计

内存管理是操作系统的重要组成部分,一个安全可靠的内存管理程序,对于操作系统的运行十分关键.采用传统软件开发方法开发的内存管理系统,安全性和可靠性得不到很好的保证.为此提出用形式化的B方法开发内存管理系统.首先使用B方法建立了内存管理的形式化模型,利用B工具对该阶段生成的证明义务进行证明,保证系统在初始规范说明层次上的内在一致性和设计的正确性.然后根据B方法分层构造的思想对上一阶段得到的抽象规范模型进行精化.最终得到一个可实现的内存管理模型,该模型更好地保证了系统的一致性和可靠性.     

用于系统级建模的DSP运算指令集设计方法

文章提出一种用于系统级建模指令集的设计方法并加以实现.该指令集作为某DSP的系统级设计建模和开发软件工具链的底层基础,为DSP的软硬件协同设计和软件模拟器的开发提供了一个平台.在工程化的测试中,通过该软件方法建立的DSP模型和硬件描述语言建立的DSP模型进行协同验证,证明了其正确性.     

系统级仿真中单片机的VHDL建模和应用

VHDL是目前通用的硬件描述语言,它支持行为级和结构级的硬件描述,其描述的层次可以从最抽象的系统级一直到可实现的逻辑级的最底层。在描述数字系统时,VHDL可以使用前后一致的语义和语法,并可以使用跨越多个级别的混合描述仿真该系统。因此,可以对由高层次行为描述和低层次详细实现组成的系统进行仿真。     

一种航空电子系统体系结构错误行为验证方法

针对航空电子系统体系结构安全性评估过程中,组件故障影响分析,正确性难以保证的问题,提出了一种基于模型的体系结构错误行为描述和验证方法。首先,针对系统功能需求和安全性目标,建立体系结构模型;然后,采用错误模型附件描述组件的错误行为和导致的故障影响,并使用层次自动机作为中间状态,通过转换算法实现体系结构错误行为模型的形式化描述;最后,通过模型检测实现安全性需求的正确性验证。实例分析表明,该方法能够验证体系结构设计的组件错误影响和应对措施是否满足系统的安全性目标,提升安全性评估的准确性和效率。     

基于组件级化简的语义验证方法在电子商务过程中的应用

工作流过程语义验证是保证过程完成其最终目的的必要方法,基于组件的语义验证方法有利于提高验证效率,适合验证大型过程的语义正确性.文章描述了在一个实际的工作流系统中,如何使用基于组件级化简的语义验证方法,对一个电子商务过程订货购买过程的三维工作流网表示进行语义验证.证明了该语义验证方法的有效性.