基于实时连续环境的嵌入式系统的模型检测技术研究

This project has a research background of using model checking technology to ensure the reliability and safety of embedded systems. It seeks for the verification method of the correctness of embedded software and hardware systems， real-time properties and the continuous nature of the embedded system. Based on the computer science, optimization mathematics and cybernetics theory, we will construct the translation rules of logic circuits to automata、embedded software codes to the executable subset of the interval temporal logic and model checking algorithms of the interval temporal logic for the verification of embedded software and hardware systems; construct translation rules of the time interval temporal logic to the real-time automata and efficient reachability analysis algorithms of real-time automata based on BDD structures for verifying real-time properties of embedded systems; and construct constrained convex polyhedron models for the reachability analysis of linear hybrid systems and computing algorithms of reachability sets based on the constraint solving、 Gaussian elimination technologies, as well as approximation algorithms and abstraction refinement rulse for translating non-linear hybrid systems to linear hybrid systems to verify continuous properties of embedded systems. These techniques will play important roles in ensuring the reliability of embedded systems, and provide amendatory feedback for the design of embedded systems.

本项目以模型检测技术在确保嵌入式系统的可靠性和安全性中的应用为研究背景，探索嵌入式系统的软硬件系统正确性以及嵌入式系统的实时性和连续性质的验证方法。基于计算机科学，优化数学以及控制学等学科的相关理论，建立逻辑电路到自动机、嵌入式软件代码到区间时序逻辑的可执行子集的转换规则和区间时序逻辑的模型检测算法进行嵌入式软硬件系统的正确性验证；建立时间区间时序逻辑到时间自动机的转换规则和基于BDD结构的时间自动机的高效的可达性分析算法验证嵌入式系统的实时性质；建立线性混合系统可达性分析的约束凸多面体模型和基于约束求解、高斯消去等技术的可达集分析算法，以及非线性混合系统到线性混合系统的近似算法和抽象加细规则用于验证嵌入式系统的连续性质。这些技术对确保嵌入式系统的可靠性和安全性将有重要作用，并可为嵌入式系统设计提供修正的反馈。

本项目研究嵌入式系统的软硬件建模方法和区间时序逻辑的模型检测算法进行嵌入式软硬件系统的正确性验证，研究时间区间时序逻辑模型检测算法验证嵌入式系统的实时性质，研究线性混合系统的可达性分析结构和非线性混合系统的近似验证算法。 取得的研究成果包括：（1）构建了基于时序逻辑语言MSVL的系统建模、仿真方法和基于区间时序逻辑的扩展--命题投影时序逻辑的系统性质验证方法；（2）通过转化为离散时间区间时序逻辑可满足性判定问题解决了实时系统的模型检测问题，解决了同一逻辑框架内无法自动验证实时系统的实时性质的问题；（3）构建了线性混合系统具有可判定的可达性问题的最大子集--矩形混合系统的可达性分析模型和算法；（4）构建了用于嵌入式穿戴设备的错误检测和数据修复的隐马尔科夫模型、贝叶斯模型和距离模型，以及基于这些模型的错误检测和数据修复算法以确保嵌入式穿戴设备的数据可靠性；（5）构建了传感器网络的防窃听模型和协作干扰方法以保证数据的可靠性；（6）建立了嵌入式通信设备中断概率测试方法和多目标免疫最优化算法；（7）提出了一种可持续性秘籍移动群智感知的拥塞感知通信范式以实现移动群智感知中的有效负载均衡和通信的可靠性。这些技术为确保嵌入式系统的可靠性和安全性提供了重要作用，同时为嵌入式系统的设计提供了修正反馈。