状态空间爆炸问题是制约模型检测应用的主要问题。基于假设/保证(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)等典型嵌入式系统中进行了应用。
{{i.achievement_title}}
数据更新时间:2023-05-31
EBPR工艺运行效果的主要影响因素及研究现状
基于国产化替代环境下高校计算机教学的研究
一种基于多层设计空间缩减策略的近似高维优化方法
复杂系统科学研究进展
基于综合治理和水文模型的广西县域石漠化小流域区划研究
基于3值抽象的假设-保证式PCTL*组合随机模型检验方法
基于扩展模糊自动机的组合Web服务验证方法研究
基于推理现象的中文文本推理资源建设和自动分析研究
基于矛盾体分离的动态自动演绎推理研究