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

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

项目编号： No.61373043

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 张海宾

作者单位： 西安电子科技大学

项目金额： 75万元

中文摘要： 本项目以模型检测技术在确保嵌入式系统的可靠性和安全性中的应用为研究背景，探索嵌入式系统的软硬件系统正确性以及嵌入式系统的实时性和连续性质的验证方法。基于计算机科学，优化数学以及控制学等学科的相关理论，建立逻辑电路到自动机、嵌入式软件代码到区间时序逻辑的可执行子集的转换规则和区间时序逻辑的模型检测算法进行嵌入式软硬件系统的正确性验证；建立时间区间时序逻辑到时间自动机的转换规则和基于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

英文关键词： embedded systems；real-time systems；hybrid systems；model checking；fault diagnosis