信息物理融合系统软件可信性验证方法研究

Cyber Physical Systems as the commanding height of information technology in the world today will be widely used in power systems, medical equipment, aerospace and other safety critical areas. Because CPS is a new kind of networked embedded systems that combine calculation process and physical environment, so it contains various and numerous embedded software which interact with each other by network, therefore, how to guarantee the trustworthiness of these software and their interaction has become one of the hotspots in CPS research area. In order to solve this problem, this study intends to integrate various forms of modeling methods and use probabilistic model checking techniques to explore the CPS software trustworthiness design and verification method, mainly includes the following two aspects: 1、To investigate the CPS software modeling method with function, time and space features based on the integration of extended deterministic and stochastic Petri net(EDSPN) and hierarchical state transition matrix(HSTM); 2、To study CPS software integrated verification method with functional verification and performance evaluation based on probabilistic model checking, meanwhile to explore multiple optimization strategies for the verification method, strive to reduce the state space explosion. The successful implementation of this subject will lay a more solid theoretical foundation for high trustworthiness CPS software development.

信息物理融合系统（Cyber Physical Systems，CPS）作为当今世界信息技术制高点，将广泛应用于电力系统、医疗仪器设备、航空航天等安全攸关领域。由于CPS是一种综合了计算进程与物理环境的新型网络化嵌入式系统，故包含种类和数目众多的嵌入式软件，且各软件通过网络交互，因此如何保障这些异构软件及其交互过程可信性已成为CPS研究热点之一。针对这一问题，本研究拟通过多种形式化建模手段融合以及概率模型检测技术，探索CPS软件可信设计与验证方法，具体包含以下两方面内容：1、研究基于扩展的确定与随机时间Petri网和层次化状态迁移矩阵相融合的CPS软件功能与时空性能一体化建模方法；2、研究基于概率模型检测的CPS软件功能与性能一体化验证方法，并针对该方法研究多种验证优化策略，力求缓解模型检测过程中的状态空间爆炸。课题的成功实施，将为高可信CPS软件开发打下更为坚实的理论基础。

信息物理系统（Cyber Physical Systems，简称CPS）作为当今世界信息技术制高点，已广泛应用于各类安全攸关领域。如何保障CPS软件可信性已成为CPS研究热点之一。本项目在软件设计阶段，研究适用于CPS软件的形式化建模方法、验证方法以及分析技术，具体解决以下四方面可信性保障问题：.针对CPS软件功能与实时性验证问题，提出基于时间状态迁移矩阵(Time State Transition Matrix, 简称TSTM)的软件形式化建模方法。TSTM在保持STM形式语义基础上，引入时钟函数与时间约束，使其适用于实时CPS软件行为刻画。在此基础上，提出了基于时间计算树逻辑的TSTM模型检测方法，为有效缓解状态空间爆炸，模型检测方法采用限界模型检测(Bounded Model Checking, 简称BMC)技术。实验表明本研究所提方法具有较好的求解效率，实现了在软件设计层面逻辑功能与时间性能的一体化建模与验证。.针对CPS软件能耗预测与分析问题，提出了基于能耗时间状态迁移矩阵(Energy Consumption Time State Transition Matrix, 简称ETSTM)的绿色软件形式化建模方法。ETSTM在TSTM基础上，引入基于软件结构特征量的能耗预测函数，并给出了基于BP神经网络的能耗预测函数拟合方法。在此基础上，提出了基于显示路径搜索和限界模型检测的CPS软件能耗多尺度分析算法，实现了在软件设计层面对CPS软件能耗的预评价。.针对CPS软件动态性能评价问题，提出了基于扩展的确定与随机Petri网(Extended Deterministic and Stochastic Petri Nets, 简称EDSPN)的CPS软件行为模型。通过为DSPN增加非确定时间语义，使其能够有效表示由中断嵌套带来的执行时间不确定问题，进而实现对中断驱动下的CPS软件行为有效建模。此外，针对EDSPN模型分析，提出了一种基于马尔科夫再生理论的模型求解方法，实现对CPS软件性能的预分析。.针对CPS软件非确定行为定量分析问题，提出了基于连续随机逻辑的EDSPN概率模型检测方法，该方法采用BMC策略。实验表明，本研究所提方法在验证局部空间可验证的软件属性时，具有较好求解效率；在验证全局空间可验证软件属性时，通过增加验证步长可逐渐逼近验证结果。