【摘 要】
：
针对嵌入式控制系统中的时序安全问题,提出一种形式化验证方法,使用证明助手Coq对嵌入式控制系统建模,并验证其时序安全性质.首先,将控制系统的运行过程描述为基于状态转移图的自动机中间模型,并建立转移关系语义公式,提高模型与系统的一致性;其次,使用线性时序逻辑将自然语言表达的安全约束转换为时序逻辑公式,消除自然语言表达的二义性;最后,在Coq中实现系统的形式化模型,将约束公式转换为Coq中的定理,并选择合适的策略进行证明.使用该方法对C语言编写的直角坐标型机器人控制系统进行建模,实验结果表明,模型满足文中设计
【机 构】
：
杭州电子科技大学网络空间安全学院,浙江杭州310018;杭州电子科技大学计算机学院,浙江杭州310018
论文部分内容阅读
针对嵌入式控制系统中的时序安全问题,提出一种形式化验证方法,使用证明助手Coq对嵌入式控制系统建模,并验证其时序安全性质.首先,将控制系统的运行过程描述为基于状态转移图的自动机中间模型,并建立转移关系语义公式,提高模型与系统的一致性;其次,使用线性时序逻辑将自然语言表达的安全约束转换为时序逻辑公式,消除自然语言表达的二义性;最后,在Coq中实现系统的形式化模型,将约束公式转换为Coq中的定理,并选择合适的策略进行证明.使用该方法对C语言编写的直角坐标型机器人控制系统进行建模,实验结果表明,模型满足文中设计提出的若干性质,发现程序中隐藏的时序安全问题并对其进行了有效修复.
其他文献
研究多值忆阻逻辑电路,采用三值忆阻逻辑运算单元,设计了三值CMOS忆阻混合型D锁存器,该三值忆阻逻辑运算单元以CMOS和电阻异质结双极性晶体管(Resistor-Heterojunction Bipolar Transistor,R-HBT)负阻型忆阻器等效模型为核心,构成的三值CMOS忆阻混合型D锁存器包括4个三值忆阻与非单元和1个三值忆阻反相器,结构简单.在忆阻D锁存器的基础上,设计了上边沿触发的三值CMOS忆阻混合型D触发器,该D触发器为主从型结构.PSPICE仿真结果符合三值D触发器的逻辑功能,验
采用计算流体力学(CFD)方法,研究φ6000 mm的大型圆筒搅拌罐体侧壁搅拌器的不同转速、安装高度、安装倾角与搅拌器数量等因素对三维流场的影响规律.结果表明单桨安装下搅拌圆筒罐体内流场产生分层,产生两个速度场方向相反的循环涡流.水平与垂直偏角的存在同时增加了整个圆筒罐体内流场的平均速度与内部流场的扰动程度,并对圆筒罐体有一定的冲刷作用,进一步加强了圆筒罐体内的混合效果.当水平偏角α=10°,垂直偏角β=7°时,单相搅拌圆筒罐体的内部流场最好,搅拌性能最佳.搅拌器安装数量N=5时,搅拌圆筒罐体内部混合性能
研究具有动态边界反馈的Timoshenko梁的能量衰减问题.首先,将系统改写成Hilbert空间上的抽象Cauchy问题,运用算子半群理论得到Timoshenko梁系统的解的存在唯一性;然后,借助乘子技巧结合频域方法证明了该系统的能量是一致指数衰减的.
探讨乳腺癌患者化疗前和化疗早期DC E-M RI影像特征与新辅助化疗疗效的关联,并利用影像特征对疗效进行预测.根据M iller-Payne分级,将61例患者划分为21例化疗有反应和40例化疗无反应;分割提取影像病灶区域特征;在留一法交叉验证下,使用支持向量机模型对疗效进行预测分析.在单变量预测分析中,化疗前和化疗早期影像最佳单特征的预测结果AUC值分别为0.749和0.779;而在进行多变量预测分析时,化疗前和化疗早期影像最优特征子集的预测结果A U C值分别为0.779和0.881.结果表明,化疗早期
物体主体结构因大面积破损失去语义信息时,无法根据破损图像已知信息有效重建物体轮廓结构并还原语义信息,为此,提出一种基于匹配图像与像素点合成纹理的物体主体结构大面积破损的图像修复算法.首先,用人工交互曲线补全破损物体缺失的结构轮廓;然后,与图像数据库进行轮廓结构匹配和颜色匹配,构建轮廓样本字典,并以人工交互曲线作引导,运用结构传达方法将轮廓样本字典传达进破损物体,修复破损物体缺失的主体结构;最后,采用基于像素点的纹理合成填充方式,分别合成填充修复前景和背景纹理,实现对破损图像的整体修复.仿真实验表明,与相关
高精度直流电刺激(High-definition Transcranial Direct Current Stimulation,HD-tDCS)可以通过靶向特定的大脑区域来调节神经活动,有益于意识障碍(Disorder of consciousness,DOC)患者的康复.追踪记录HD-tDCS治疗的27例DOC患者在4个治疗阶段的昏迷恢复量表(Coma Recovery Scale-Revised,CRS-R)评分和脑电图,探究HD-tDCS对DOC患者脑电特征变化的影响.研究结果发现,经过HD-tD
研究了一类具有数据丢包及随机网络诱导时滞的线性网络控制系统稳定性问题.首先,根据Lyapunov稳定性理论,加入增广矩阵和三重积分项,构造一个改进的Lyapunov泛函;其次,使用Wirtinger不等式、凸组合引理和Jensen不等式处理泛函求导过程中产生的积分项,并结合广义Finsler引理,以线性矩阵不等式形式给出保守性较小的稳定性准则.最后,数值算例验证了所给出准则的有效性.
提出并分析一类非线性离散等级结构种群模型.证明了解的非负有界性,定义了基本再生数,建立了种群正平衡态的存在唯一性,并运用非负矩阵特征值理论获得了零平衡态的渐近稳定性与不稳定性条件.
随着变频技术的引入,压缩式制冷系统存在工况范围大、干扰多、非线性、运行参数强耦合等问题,简单控制方法无法保证系统稳定高效运行,开发合适的控制算法是保障变频压缩式制冷系统节能高效运行的关键.文章结合近年来国内外相关研究,从比例积分微分(Proportional-integral-derivative,PID)控制、最优控制、智能控制方法出发,介绍适用于变频压缩式制冷系统的先进控制方法,并根据目前研究的不足,提出变频压缩式制冷系统控制研究未来发展建议.
为了提高射雾器的射程,同时提高Kriging代理模型的优化效率和精度,提出一种新的自适应代理优化算法,包括全局探索阶段和局部探索阶段.在全局探索阶段,提出改进的最大期望概率提高准则(Improved Probability Improvement,IPI)和并行加点策略;在局部探索阶段,通过最小响应面准则(Minimizing Prediction,MP)获取新样本点;各加点准则均采用差分进化算法进行寻优,并根据新样本点和已知样本点的关系来实现全局探索和局部探索的自适应切换,直至找到最优解.算例实验表明: