关键词:
离散事件系统
有限自动机
形式化方法
矩阵半张量积
不透明性
能观性
故障可诊断性
故障预诊断性
摘要:
信息物理系统(CPSs)研究正成为支撑各个产业信息化提升以及产业间深度交叉融合的关键技术,但因为网络环境的复杂性,信息安全与隐私保护成为实现CPSs功能安全的重要保障,也是相关技术研究中的重点和难点。以离散事件系统(DESs)建模CPSs的高阶行为,分析讨论其安全性相关问题是一个有意义且深受关注的课题。论文基于形式化方法和代数状态空间方法研究了有限自动机模型下的DESs不透明性、能观性、故障可诊断性、故障预诊断性等安全相关问题。具体地,论文主要工作包括以下几个方面:
(1)关于DESs的不透明性问题:针对更复杂的现实环境和更严格的安全性要求,提出了三种新的强不透明性定义,即强W、(W,M)和(W,∞)不透明性,通过构造一种带有标签的W-受限状态估计器,实现了三种强不透明性的验证。与已有的不透明性定义相比,三个新定义增加了对系统的安全性量化功能,特别地,强(W,M)和(W,∞)不透明性首次综合了当前信息、延时信息和预测性进行分析,提高了系统的安全性要求。
(2)关于DESs的不透明性加强问题:针对不能自然地满足强(W,∞)不透明性的系统,提出了强(Wmax,∞)不透明性的概念,并给出了验证和求解Wmax的方法。根据“防御+反击”的强(Wmax,∞)不透明性加强目标,针对有效的替换函数提出了私立智能安全性的定义,构造了Wmax-受限替换-状态观测器,并在此基础上给出了有效的替换函数存在的充分必要条件。新的不透明性加强目标具有保护秘密信息不被暴露和诱导隐秘入侵者暴露身份的双重安全属性。
(3)关于DESs的能观性问题:针对结构更复杂的并联、串联和反馈合成自动机,利用矩阵半张量积建立了结构一致的代数模型,构造了初始状态-输出关联多项式矩阵和当前状态-输出关联多项式矩阵,并基于两个多项式矩阵给出了验证四种能观性的充要条件和算法。所提算法主要依赖于矩阵操作,易于计算机实现。
(4)关于DESs的故障可诊断性问题:针对由状态转移耦合形成的并联和乘积复合自动机,利用半张量积理论分别建立了结构一致的代数表达式。考虑一种新的故障形式,提出了基于代数状态空间的故障可诊断性的新定义。构造了矩阵观测器来验证系统是否故障可诊断,并给出了相应的算法。矩阵方法刻画形式简单,为离散事件系统故障可诊断性研究提供了新的思路。
(5)关于DESs的故障预诊断性问题:针对具有(M,K)性能界的分散式预诊断器的存在问题,提出了基于状态估计的更广义的SE-协预诊断性概念,并针对三种不同情况设计了相应的分散式故障预诊断器。将形式化方法与代数状态空间方法相结合,提出了新的状态估计算法,并在此基础上解决了SE-协预诊断性的验证问题。考虑到通信信道的可靠性问题,提出了z-可靠SE-协预诊断性的概念,并设计出有效的z-可靠分散式预诊断器。