卫星定位系统的验证原型

用模型检查的方法对卫星定位系统进行了验证,对把模型检查应用于实际系统进行了初步的探索。     

线性混合系统的一种验证方法

混合系统是指嵌入于物理环境中的数字实时系统．由于计算机技术的快速发展,混合系统在各行各业中都得到广泛应用,但是由于混合系统涉及到连续时间,因此其验证问题始终没有得到完善的解决．近年来,人们普遍采用模型检验方法对混合系统进行验证．由于线性混合系统在实际应用中可以表示大多数的嵌入式实时系统,因此我们着重研究这类混合系统的验证算法．本文首先介绍了混合系统的模型—混合自动机,然后提出了一种针对线性混合系统的基于区域的先划分再遍历的半确定性验证方法．经实例检验,该方法能够有效地验证线性混合系统．最后将本文的方法同有关的其它算法进行了比较     

时间自动机的事务级形式验证

提出了一种形式方法用于验证TLM-2.0的设计方案.该方法中TLM-2.0设计方案将被转换成定时自动机形式模型.定义若干种属性,验证将根据这些属性执行,并引入一种模拟事务级设计方案差错的故障模型来评估这些属性.然后这些属性通过使用形式UPPAAL验证工具在系统的定时自动机表示上针对这些故障被验证.最后通过一个实例研究说明该方法的有效性.     

线性混合系统符号模型验证中的参数分析方法

说明了ＨＹＴＥＣＨ工具中采用的参数分析方法对系统描述能力的限制，提出了分离参数变量和系统状态变量的符号模型检查算法，并对用ＨＹＴＥＣＨ不能分析的Ｆｉｓｃｈｅｒ互斥算法的时钟偏移的界进行了分析。     

基于CheckMate的混合系统建模和验证

形式验证是混合系统中的重要研究方向,Checkmate是基于MATLAB/Simulink和Stateflow工具箱开发的一种混合系统建模、仿真和形式验证工具。文章首先介绍了混合系统形式验证的概念和验证过程,从用户的角度介绍了CheckMate的每个自定义模块的设置及其功能原理,通过一个三维线性混合系统的例子,说明了使用CheckMate进行建模、仿真以及验证的方法,最后指出了CheckMate验证工具的局限性。     

基于混成自动机的CPS行为建模与属性验证

系统实时性、安全性和可靠性等非功能属性是信息物理系统在诸多领域应用的关键因素。论文在分析CPS模型构建与分析验证中面临的挑战的基础上,提出了一种CPS行为建模与属性验证方法。该方法首先基于混成自动机对CPS的行为进行建模,然后将此模型转换为混合程序模型,最后在定理证明器KeYmaera中对HP模型的属性进行形式化验证。文中论述了行为模型描述语言的结构,建立了混成自动机模型与HP模型之间的转换规则,分析了模型转换的一致性。应用实例表明:该方法既能简单直观地描述CPS动态行为,又能对CPS的属性进行严格的形式化验证,且有效避免了形式化验证中的状态空间爆炸问题。     

基于流管道过近似的混合系统形式化验证技术

文章针对混合系统形式验证中可达集计算的问题,介绍了通过流管道过近似的方法计算系统可达集的基本原理,给出了具体的计算过程;结合一个切换系统的实例,建立其混合自动机模型,在MATLAB语言环境下编程,实现验证过程.     

基于切换表面状态划分的倒立摆模型验证

针对仿真对不存在或难以寻找的问题,利用商迁移系统,给出了混合系统的验证过程。结合倒立摆模型给出的只对状态空间切换表面进行离散化的空间划分方法,相对于常规验证所采用的离散整个连续状态空间的方法,降低了系统分析的维数。提出将阈值切换切分为两类,明确了切换面的划分方式。     

500万t/a常减压装置常压塔顶换热器、常压炉局部改造

随着加工原油的轻质化,兰州石化公司500万t/a常减压装置常压塔顶负荷达到上限,常压塔的操作压力高达0.150MPa,常压塔顶常顶油气-热媒水换热器E-504出口温度上升,部分油气相变直接后移至空冷器,对空冷器的腐蚀加剧;换热终温下降,常压炉负荷上升,对流室取热不足,常压炉热效率长期较低。为此,对常压塔顶热媒水换热器以及常压炉对流室炉管进行了技术改造,降低了常压塔的操作压力,空冷器的腐蚀明显改善,常压加热炉效率上升。     

通信协议形式验证中的Petri网方法

Petri网,尤其是扩充类的Petri网对通信协议有很强的模拟能力.同时,Petri网能支持十分有效的验证技术.本文分析了需要验证的协议性质,提出了用线性不变量和标志机状态法全面分析这些性质的综合验证方法,并给出了对HDLC通信协议的验证实例.     

焦炉立火道温度控制研究

研究了焦炉加热自适应控制算法,结合马鞍山钢铁公司煤焦化公司6^#焦炉加热的计算机串级控制系统,建立了温度控制系统的最优化控制模型,实践表明,该系统可靠,炉温稳定,节能明显。     

操作系统形式化验证综述

介绍操作系统验证理论、语言和工具等技术基础,阐述验证路径、精化关系验证和大规模验证等新的验证方法和理念.比较分析多个操作系统验证项目研究内容、验证方法、主要贡献以及最新进展.分析操作系统验证过程中存在的问题,认为验证成本高、验证工具局限性是制约操作系统形式化验证的关键因素,随着验证工具、框架和定理库的完善,以及深度学习...     

一个信息安全系统的形式描述和验证

本文通过引入一些新概念，利用有限状态机原理和BLP模型、Biba模型思想，对一个基于认证和授权的信息系统进行了形式化描述和验证，该模型具有保密性和完整性。     

全负压焦炉煤气处理系统

为了说明全负压流程的优点，本文用框图对焦炉煤气处理系统在正压下和在负压下进行了比较，并在全面介绍全负压焦炉煤气处理系统基础上，详细叙述了负压流程的优点.在我国石家庄焦化厂已得到应用，芜湖市城市煤气第三期气源工程也已正常投入运行，各项指标均已达到或超过了设计要求.     

一种基于时间自动机网络的实时系统形式化验证方法

介绍了时间自动机形式模型,在此基础上给出了时间自动机网络的形式语法和语义,然后给出一种基于时间自动机网络的实时系统形式化验证方法,并采用基于时间自动机网络的模型检测工具UPPAAL对一个经典的实时系统实例进行了验证．     

形式验证中近似流管道的算法研究

混合系统形式验证技术是分析在给定的初始条件下,系统的可达集是否都在目标状态集合内。计算可达集是混合系统形式验证中的重要一步,选用何种几何体表示可达集对于整个验证精度有决定性的影响。文章对有向矩形壳和凸多面体2种状态可达集近似表示方法进行了分析比较,结合2种方法的优点提出了流管道过近似混合算法以降低保守性和提高运算速度;最后在Matlab环境下实现了混合算法并且验证了1个分段非线性系统实例,验证结果显示了所提混合算法的有效性。     

焦炉集气管压力智能协调控制系统及其应用

根据集气管系统的工艺流程和动态特性,提出了一种分层智能协调控制方法,将集气管控制系统划分为3个层次:基础控制级,解耦级和协调级.通过分层结构处理过程的复杂性,实现算法的模块化,便于算法设计、调试、使用和维护.采用了基于多变量模型辨识的解耦控制,并通过协调专家系统协调各层次的控制行为,提高控制系统整体的适应性、可靠性,改善控制品质.基于西门子S7软硬件系统的实现了智能协调控制系统,实际应用取得了良好的效果.     

可变加热速率线网反应器设计及验证

为了研究温度历程对气固反应的影响,根据可调加热速率和恒温温度的反应器的要求,设计了线网反应器的结构和控制电路.通过对所搭建的线网反应器实验台进行温度标定,并且进行实验,得到不同的升温速率和最高恒温温度对于煤热解特性的影响,通过与实验结果进行比较后,验证了反应器的可靠性.线网反应器实现了0~1 000 K/s的可调加热速率,并可在1 000 ℃以下的设定温度保持给定的停留时间,大大强化了对气固反应的研究能力.     

压力容器可靠性设计与检验

本文阐述了可靠性设计在压力容器设计中的重要性。介绍了常规设计与可靠性设计的区别、可靠性设计的概率统计基础、设计参量的统计处理以及压力容器可靠性设计的内容和步骤。用算例邦助读者掌握计算方法,并由实验加以验证。