基于UPPAAL的FAO系统典型运营场景建模与验证

全自动驾驶系统FAO(Fully Automatic Operation)具有安全、可靠、高效的特点,成为未来城市轨道智能交通系统的主要发展方向。FAO系统典型运营场景是1个实时的过程,为发现其逻辑的错误、功能和性能的缺陷,需要在系统设计前,针对系统需求规范中典型运营场景的实现流程进行形式化分析。本文分析FAO典型运营场景保护区的实现流程,在系统需求规范中提取其功能与性能的需求,采用基于时间自动机理论的UPPAAL构建时间自动机网络模型,进行仿真分析,并验证其功能属性、性能属性与安全属性。通过反例分析、模型修正,增强对FAO系统的理解,减少设计故障,提高安全性,为系统设计与实现打下良好的基础。

假数据注入攻击下信息物理融合系统的稳定性研究

假数据注入(False data injection, FDI)攻击由于其隐蔽性特点,严重威胁着信息物理融合系统(Cyber-physical systems, CPS)的安全.从攻击者角度,本文主要研究了FDI攻击对CPS稳定性的影响.首先,给出了FDI攻击模型,从前向通道和反馈通道分别注入控制假数据和测量假数据.接着,提出了FDI攻击效力模型来量化FDI攻击对CPS状态估计值和测量残差的影响.在此基础上,设计了一个攻击向量协同策略,并从理论上分析出操纵CPS稳定性的攻击条件:攻击矩阵H和系统矩阵A的稳定性及时间参数ka的选取时机.数值仿真结果表明FDI攻击协同策略能够有效操纵两类(含有稳定和不稳定受控对象)系统的稳定性.该研究进一步揭示了FDI攻击的协同性,对保护CPS安全和防御网络攻击提供了重要参考.