混合系统的分析

在人们日常生活中,混合系统(Hybrid Sstem)应用的实例很多,如汽车中的计算机控制系统、飞机中的平稳飞行痤制系统等都属于混合系统的范畴,并且随着计算机技术的发展,混合系统的应用范围会更加广泛,入们的生活会更加依赖于混合系统,固此社会应用的需求要求研究人员对混合系统进行比较深入的研究,保证混合系统运行的正确性。

常压炉加热系统形式建模的验证

文章运用基于流管道的混合动态系统形式验证方法,解决了常压炉加热系统工艺参数的验证问题;通过对常压炉加热系统的运行机理进行分析并建立混合自动机模型,应用状态可达集的过近似方法计算近似流管道;通过对近似流管道的分析,验证常压炉加热系统设定的燃料流量是否满足生产工艺要求;经多次验证,最终得到了燃料流量的取值范围。

基于多面体包含的非线性混成系统可达性分析

针对一类非线性混成系统的可达性问题,提出了一种基于多面体包含的分析方法。首先介绍了混成系统及其可达性,讨论了如何应用多面体包含对多项式混成系统进行线性近似,并采用量词消去和非线性优化方法来构造相应的线性混成系统,然后运用验证工具SpaceEx求得原非线性混成系统的过近似可达集,并应用于验证系统的安全性。

基于迁移系统分析的线性混成系统安全验证

混成自动机行为中既包含离散行为又包含连续行为,非常复杂。其安全性验证问题难以解决,即使是线性混成自动机,它的可达性问题也被证明是不可判定的。现有工具大都使用多面体计算来计算线性混成自动机的可达状态空间集,复杂度高,可处理问题规模非常有限。为了避免这类问题,实现了一种新的工具。该工具将线性混成自动机表达为等价的迁移系统,并利用迁移系统上不变式生成相关工作对混成自动机进行验证。实验数据表明,方法有效可行,工具具有良好的性能。

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

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

基于控制周期特征式的线性混合自动机验证

提出了一种基于归纳法思想的验证方法 ,通过控制周期上特性的描述 ,发现了基于控制周期特征式的线性混合自动机验证方法。这一方法采用定理证明过程来得出归纳证明的结构 ;采用模型检查方法来得出归纳证明的奠基和迭代步。这一方法同时兼顾了模型检查和定理证明的特点 ,用此定理证明更高的自动化程度解决了单用模型检查不能解决的问题 ,得出了对著名案例 GasBurner问题中的参数 3non- leakking≥ 76的最优范围。

材料非线性对混合陶瓷球轴承有限元分析的影响

重点研究了材料非线性行为在有限元法分析混合陶瓷球轴承接触问题中的影响。首先对混合陶瓷轴承中的轴承钢GCr15进行了材料单轴拉伸试验,以确定其材料性能参数,再通过对几种接触模型的材料线性和材料非线性有限元分析、试验研究和赫兹接触理论计算,将这些结果比较分析,得到材料非线性对有限元接触分析在不同情况下的影响,从而对材料非线性行为在有限元接触分析中的应用做出评估。

一种中断驱动系统的时间约束验证方法

中断是嵌入式系统进行实时响应的重要机制.以测试为基础的传统方法在处理中断驱动的系统时,由于系统可能的运行轨迹空间无穷,其有效性受到很大的影响.本文基于线性混成自动机有界验证技术提出一种对中断驱动系统的时间约束进行验证的方法,应用线性混成自动机对中断驱动的系统建模,将时间约束验证问题转换成线性混成自动机上的路径可达性判定问题,并借助模型检验工具BACH来进行验证,以周期性中断源驱动的嵌入式系统为例,说明了方法的可行性和有效性.