基于假设/保证自动推理的组合验证研究

基本信息
批准号:60903030
项目类别:青年科学基金项目
资助金额:17.00
负责人:贺飞
学科分类:
依托单位:清华大学
批准年份:2009
结题年份:2012
起止时间:2010-01-01 - 2012-12-31
项目状态: 已结题
项目参与者:荔建琦,王瑞,周旻,尹良泽,祝鹤,朱振
关键词:
假设/保证嵌入式系统模型检测组合验证抽象精化
结项摘要

状态空间爆炸问题是制约模型检测应用的主要问题。基于假设/保证(Assume/Guarantee,简称A/G)规则的自动推理框架被认为是最有前途的组合验证方法学之一,具有非常重要的理论与应用价值。区别于一般的A/G组合验证,该框架能够完全自动化。该技术的研究在国际上仍是崭新且富有挑战性的,有很多问题尚未解决。本课题拟对该技术的三个基本问题展开研究,即A/G自动推理框架、模型自动分解算法和符号化模型检测算法。此外,本课题还将从应用角度对该技术进行探讨,将基于接口自动机对该理论进行扩展,并将其应用到典型嵌入式系统的验证之中。

项目摘要

状态空间爆炸问题是制约模型检测应用的主要问题。基于假设/保证(Assume/Guarantee,简称A/G)规则的自动推理框架被认为是最有前途的组合验证方法学之一,具有非常重要的理论与应用价值。本课题对该技术的三个基本问题展开研究,即A/G自动推理框架、模型自动分解算法和符号化模型检测算法。主要研究内容包括:模型自动分解算法、A/G自动推理框架、基于其他自动机的扩展、符号化验证算法、符号化验证引擎等。本项目达到并部分超过了预期的目标,至今已发表学术论文8篇(包括IEEE Transactions on Computers 2篇,本领域顶级会议CAV 1篇)。设计并实现了一个面向构件化嵌入式系统的模型检测工具VCS,并且在门仓控制系统、多功能车辆总线控制器(MVBC)等典型嵌入式系统中进行了应用。

项目成果
{{index+1}}

{{i.achievement_title}}

{{i.achievement_title}}

DOI:{{i.doi}}
发表时间:{{i.publish_year}}

暂无此项成果

数据更新时间:2023-05-31

其他相关文献

1

EBPR工艺运行效果的主要影响因素及研究现状

EBPR工艺运行效果的主要影响因素及研究现状

DOI:10.16796/j.cnki.1000-3770.2022.03.003
发表时间:2022
2

基于国产化替代环境下高校计算机教学的研究

基于国产化替代环境下高校计算机教学的研究

DOI:
发表时间:
3

一种基于多层设计空间缩减策略的近似高维优化方法

一种基于多层设计空间缩减策略的近似高维优化方法

DOI:10.1051/jnwpu/20213920292
发表时间:2021
4

复杂系统科学研究进展

复杂系统科学研究进展

DOI:10.12202/j.0476-0301.2022178
发表时间:2022
5

基于综合治理和水文模型的广西县域石漠化小流域区划研究

基于综合治理和水文模型的广西县域石漠化小流域区划研究

DOI:10.14050/j.cnki.1672-9250.2017.02.014
发表时间:2017

贺飞的其他基金

批准号:41206130
批准年份:2012
资助金额:27.00
项目类别:青年科学基金项目
批准号:11801474
批准年份:2018
资助金额:26.00
项目类别:青年科学基金项目
批准号:61272001
批准年份:2012
资助金额:61.00
项目类别:面上项目
批准号:61672310
批准年份:2016
资助金额:64.00
项目类别:面上项目
批准号:31470236
批准年份:2014
资助金额:82.00
项目类别:面上项目
批准号:11561049
批准年份:2015
资助金额:35.00
项目类别:地区科学基金项目
批准号:51602072
批准年份:2016
资助金额:21.00
项目类别:青年科学基金项目

相似国自然基金

1

基于3值抽象的假设-保证式PCTL*组合随机模型检验方法

批准号:61303022
批准年份:2013
负责人:刘阳
学科分类:F0203
资助金额:26.00
项目类别:青年科学基金项目
2

基于扩展模糊自动机的组合Web服务验证方法研究

批准号:61003061
批准年份:2010
负责人:雷丽晖
学科分类:F0203
资助金额:20.00
项目类别:青年科学基金项目
3

基于推理现象的中文文本推理资源建设和自动分析研究

批准号:61402341
批准年份:2014
负责人:任函
学科分类:F0211
资助金额:26.00
项目类别:青年科学基金项目
4

基于矛盾体分离的动态自动演绎推理研究

批准号:61673320
批准年份:2016
负责人:徐扬
学科分类:F0601
资助金额:59.00
项目类别:面上项目