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

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

项目编号： No.60973049

项目类型： 面上项目

立项/批准年度： 2010

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

项目作者： 罗贵明

作者单位： 清华大学

项目金额： 33万元

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

中文关键词： 模型检测；自适应算法；形式化建模；加权自动机；

英文摘要：

英文关键词： Model checking；adaptive algorithms；formal modeling；weighted automata；