可编程嵌入式系统形式化建模与自动验证技术的研究

结题报告

项目介绍

AI项目解读

基本信息

批准号：
60973049
项目类别：
面上项目
资助金额：
33.0万
负责人：
罗贵明
依托单位：
清华大学
学科分类：
F0204.计算机系统结构与硬件技术
结题年份：
2012
批准年份：
2009
项目状态：
已结题
起止时间：
2010-01-01 至2012-12-31

项目参与者：
黄红选；郭陟；贺飞；李力；范丹；金明；赵玥；郑岳山；张俊杰；
关键词：
可编程嵌入式系统形式化建模可靠性模型检测

项目摘要

可编程嵌入式系统能更好地满足工程的需要，在众多行业中得到广泛使用。随着计算技术的发展，嵌入式软件的规模和复杂性不断增加，计算系统的可靠性更显得重要。模型检测技术能验证一个系统是否满足其属性，查找系统出现的错误，从而降低由于在系统部署前未发现错误而导致灾难性后果的风险。本项目研究可编程嵌入式系统计算技术的可靠性。提取系统关键的属性，采用形式化方法对嵌入式系统建模、抽象、精化和自动检测。利用自适应技术探讨嵌入式软件黑箱模型的自适应建模理论和检测方法。研究模型和属性的分解，提出系统和组件一致性的验证方法。将可满足度方法用于模型检测中，建立基于可满足度的推理框架可信的网络推理系统；改进UML模型检测工具，提出一个检测UML模型的验证方法。改进自动机转换和优化验证搜索算法，减少自动机状态数量，缓解状态爆炸问题。应用本项目的理论和方法，建立和完善嵌入式系统的模型检测工具，并对实际PLC系统作检测验证。

结项摘要

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