【摘 要】
：
系统实时性、安全性和可靠性等非功能属性是信息物理系统在诸多领域应用的关键因素。论文在分析CPS模型构建与分析验证中面临的挑战的基础上,提出了一种CPS行为建模与属性验
【机 构】
：
西北工业大学计算机学院,空军工程大学理学院
【基金项目】
：
国家自然科学基金（61472443）
论文部分内容阅读
系统实时性、安全性和可靠性等非功能属性是信息物理系统在诸多领域应用的关键因素。论文在分析CPS模型构建与分析验证中面临的挑战的基础上,提出了一种CPS行为建模与属性验证方法。该方法首先基于混成自动机对CPS的行为进行建模,然后将此模型转换为混合程序模型,最后在定理证明器KeYmaera中对HP模型的属性进行形式化验证。文中论述了行为模型描述语言的结构,建立了混成自动机模型与HP模型之间的转换规则,分析了模型转换的一致性。应用实例表明：该方法既能简单直观地描述CPS动态行为,又能对CPS的属性进行严格的形式
其他文献
研究了具有加权平均预测的一阶多智能体系统一致性的采样控制问题。应用时滞分解技术得到了基于采样数据的离散时间一致性协议,同时,使用代数图论、线性系统的稳定性理论,获
针对4-WFRFT隐蔽通信系统，非目的接收机在一定时间内仍能有效的通过参数扫描获得解调参数的不足，提出了一种采用双层多项多参数加权分数阶傅里叶变换（DL-MPWFEFT）与星座扰乱的卫
为提高变换域通信系统多址接入性能,降低系统误比特率,提出基于改进型Logistic混沌序列的变换域扩频编码通信系统。利用扩频序列优选原则,选取改进型Logistic混沌序列作为扩
针对FRFT-TDCS采用传统门限设置方法时难以有效剔除多分量LFM干扰的问题，提出了基于噪声估计的FRFT—TDCS门限设计方法。该方法在分析FRFT域内LFM干扰信号和噪声频谱分布特征
以二氰二胺为氮掺杂剂，采用溶胶凝胶法制备了氮掺杂碳包覆LiFeP04的复合材料，并且分析了氮掺杂量对电极材料结构与性能的影响。研究结果表明，柠檬酸和二氰二胺在高温下的原位分
在机载非正侧MIMO 雷达系统中，传统统计类空时自适应处理方法难以获得足量的独立同分布训练单元，无法准确估计待测单元杂波特性，杂波抑制性能严重下降。为了减少所需训练单元数，
借鉴干涉式逆合成孔径雷达中多天线干涉处理的思想，采用L型三天线成像结构，提出了一种基于多天线干涉处理的窄带雷达空间旋转目标三维成像方法。推导了窄带条件下空间旋转目标
侵彻的巨大动能会对结构造成毁伤,准确预测弹体侵彻地下洞室的毁伤效应,对地下防护工程的设计具有重要意义。针对当前方法存在的问题,提出了改进型灰狼算法优化最小二乘法支
无源探测系统、电子干扰等威胁使得射频隐身性能成为制约机载雷达效能发挥的关键,对于机载雷达射频隐身性能评估也变得愈发重要。针对施里海尔截获因子评估机载雷达射频隐身
为提高飞机上作动系统的功率预测精度,建立了改进的多变量灰色神经网络预测模型。考虑了对系统功率需求有较大影响的相关因素,采用主成分分析法提取综合变量作为输入,在提升