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

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.