项目简介
项目名称
可编程嵌入式系统形式化建模与自动验证技术的研究
项目批准号
60973049
学科分类
F020307
信息科学部
_计算机科学
_计算机体系结构
_计算系统可靠性
资助类型
信息科学
负责人
罗贵明
依托单位
清华大学
批准年份
2009
起止时间
201001-201212
批准金额
33.00万元
摘要
可编程嵌入式系统能更好地满足工程的需要，在众多行业中得到广泛使用。随着计算技术的发展，嵌入式软件的规模和复杂性不断增加，计算系统的可靠性更显得重要。模型检测技术能验证一个系统是否满足其属性，查找系统出现的错误，从而降低由于在系统部署前未发现错误而导致灾难性后果的风险。本项目研究可编程嵌入式系统计算技术的可靠性。提取系统关键的属性，采用形式化方法对嵌入式系统建模、抽象、精化和自动检测。利用自适应技术探讨嵌入式软件黑箱模型的自适应建模理论和检测方法。研究模型和属性的分解，提出系统和组件一致性的验证方法。将可满足度方法用于模型检测中，建立基于可满足度的推理框架可信的网络推理系统；改进UML模型检测工具，提出一个检测UML模型的验证方法。改进自动机转换和优化验证搜索算法，减少自动机状态数量，缓解状态爆炸问题。应用本项目的理论和方法，建立和完善嵌入式系统的模型检测工具，并对实际PLC系统作检测验证。
评论区 (0)
#插入话题
