本项目研究可编程嵌入式系统计算技术的可靠性。研究了复杂系统的自适应建模算法和嵌入式软件黑箱模型的自适应建模理论和检测方法。利用SVM和神经网络研究了系统建模方法，提出了适合不同需求的自适应算法；改进了可满足度求解算法，研究了时序逻辑的可满足度；利用可满足度理论研究了推理框架；对模型检测及算法作了深入的研究，给出时序逻辑到自动机的直接转换算法，将LTL 公式一次性转换为基于迁移的Büchi 自动机。研究了嵌入式系统的环境建模和时间自动机建模，提出了环境的划分与合并的算法、时间抽象和建模的方法。将加权自动机用于组合电路的时序建模，提出了事件传播加权自动机模型。研究了UML状态图的随机和连续时间属性。分析了带有时间自动机的CSL语言，将时间属性引入检测体系，并将其和带有命题和概率的状态图结合起来，提出了针对状态图的随机和时间属性的模型检测方法。对全称CTL给出了有界模型检测方法，给出了逻辑公式对无界情形的检测特点和证据满足的条件。提出了模块建模与模型检测一体化检测方法，并设计模型检测工具，对可编程嵌入式软件进行检测。