面向软件演化的回归形式化验证研究

结题报告
项目介绍
AI项目解读

基本信息

  • 批准号：
    61672310
  • 项目类别：
    面上项目
  • 资助金额：
    64.0万
  • 负责人：
    贺飞
  • 依托单位：
    清华大学
  • 学科分类：
    F0201.计算机科学的基础理论
  • 结题年份：
    2020
  • 批准年份：
    2016
  • 项目状态：
    已结题
  • 起止时间：
    2017-01-01 至2020-12-31

项目摘要

The development of modern software cannot be accomplished in an action, but needs an incremental and evolving procedure. It is important to develop efficient techniques to formally verify evolving software systems. Regression formal verification is being considered as a promising approach for this purpose. This technique is still new and remains challenging. It is valuable both to theory and practice. This project mainly addresses the following techniques: regression model checking, regression compositional verification and regression program analysis. The project will develop a regression verification tool for evolving software systems, which will be applied to the verification of driver programs.
现代软件的开发已经不再是一蹴而就式，而是生长演化式的。适应于软件的持续改变与演化，开发高效的形式化验证技术具有重要意义。回归形式化验证是应对这一问题的有效途径。该技术的研究在国际上仍是崭新且富有挑战性的，具有重要的理论与应用价值。本课题拟开展回归模型检测、回归组合验证和回归程序分析的研究。以此为基础设计面向软件演化的回归验证工具，并在驱动程序验证中进行应用。

结项摘要

现代软件的开发已经不再是一蹴而就式，而是生长演化式的。适应软件的持续改变与演化，开发高效的形式化验证技术具有重要意义。本课题研究面向软件演化的回归形式化验证技术，首次提出了增量式程序终止性证明和回归组合验证的想法；设计并实现了增量式程序抽象和增量式程序分析等回归验证技术。此外，在程序验证的硬核问题（循环不变式生成、终止性证明、约束求解）上也取得了重要进展。基于上述成果，开发了程序验证工具Ceagle，并在驱动程序验证中进行了应用。

项目成果

期刊论文数量（10）
专著数量（0）
科研奖励数量（0）
会议论文数量（6）
专利数量（0）
Efficient software product-line model checking using induction and a SAT solver
使用归纳法和 SAT 求解器进行高效的软件产品线模型检查
  • DOI：
    10.1007/s11704-016-6048-7
  • 发表时间：
    2018-02
  • 期刊：
    Frontiers of Computer Science
  • 影响因子：
    4.2
  • 作者：
    He Fei;Gao Yuan;Yin Liangze
  • 通讯作者：
    Yin Liangze
Efficient Summary Reuse for Software Regression Verification
软件回归验证的高效摘要重用
  • DOI：
    10.1109/tse.2020.3021477
  • 发表时间：
    2022-04
  • 期刊：
    IEEE Transactions on Software Engineering
  • 影响因子：
    7.4
  • 作者：
    Fei He;Qianshan Yu;Liming Cai
  • 通讯作者：
    Liming Cai
基于扩展标记变迁模型的时钟同步协议正确性验证
  • DOI：
    --
  • 发表时间：
    2019
  • 期刊：
    国防科技大学学报
  • 影响因子：
    --
  • 作者：
    曲国远;徐晓飞;刘威廷;王沁煜;贺飞
  • 通讯作者：
    贺飞
Conflict resolution for structured merge via version space algebra
通过版本空间代数解决结构化合并的冲突
  • DOI：
    10.1145/3276536
  • 发表时间：
    2018-10
  • 期刊：
    Proceedings of the ACM on Programming Languages
  • 影响因子：
    --
  • 作者：
    Zhu Fengmin;He Fei
  • 通讯作者：
    He Fei
Inferring software behavioral models with MapReduce
使用 MapReduce 推断软件行为模型
  • DOI：
    10.1016/j.scico.2017.04.004
  • 发表时间：
    2017-10-01
  • 期刊：
    SCIENCE OF COMPUTER PROGRAMMING
  • 影响因子：
    1.3
  • 作者：
    Luo, Chen;He, Fei;Ghezzi, Carlo
  • 通讯作者：
    Ghezzi, Carlo

数据更新时间：{{ journalArticles.updateTime }}

{{ item.title }}
{{ item.translation_title }}
  • DOI：
    {{ item.doi || "--"}}
  • 发表时间：
    {{ item.publish_year || "--" }}
  • 期刊：
    {{ item.journal_name }}
  • 影响因子：
    {{ item.factor || "--"}}
  • 作者：
    {{ item.authors }}
  • 通讯作者：
    {{ item.author }}

数据更新时间：{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ monograph.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ patent.updateTime }}

其他文献

衰老大鼠睾丸组织受何首乌饮调控差异表达基因的筛选
  • DOI：
    10.3969/j.issn.1008-0805.2017.07.016
  • 发表时间：
    2017
  • 期刊：
    时珍国医国药
  • 影响因子：
    --
  • 作者：
    回陈红;刘昊坤;杜云帆;秦瑄希;徐天戎;贺飞;牛嗣云
  • 通讯作者：
    牛嗣云
模糊距离空间 中的循环 phi-压缩映射的不动点定理
  • DOI：
    --
  • 发表时间：
    2018
  • 期刊：
    数学的实践与认识
  • 影响因子：
    --
  • 作者：
    路宁;贺飞;樊菁菁
  • 通讯作者：
    樊菁菁
学习加权自动机
  • DOI：
    --
  • 发表时间：
    2014
  • 期刊：
    计算机工程与设计
  • 影响因子：
    --
  • 作者：
    惠涵;贺飞;顾明
  • 通讯作者：
    顾明
模糊距离空间中Meir-Keeler型不动点定理
  • DOI：
    --
  • 发表时间：
    2018
  • 期刊：
    内蒙古大学学报（自然科学版）
  • 影响因子：
    --
  • 作者：
    樊菁菁;贺飞
  • 通讯作者：
    贺飞
b-距离空间中 alpha-(phi, psi) 压缩重合点定理
  • DOI：
    --
  • 发表时间：
    2017
  • 期刊：
    大学数学
  • 影响因子：
    --
  • 作者：
    李淑方;贺飞;杜丽蔓
  • 通讯作者：
    杜丽蔓

其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI：
    {{ item.doi || "--" }}
  • 发表时间：
    {{ item.publish_year || "--"}}
  • 期刊：
    {{ item.journal_name }}
  • 影响因子：
    {{ item.factor || "--" }}
  • 作者：
    {{ item.authors }}
  • 通讯作者：
    {{ item.author }}
empty
内容获取失败，请点击重试
重试联系客服
title开始分析
查看分析示例
此项目为已结题，我已根据课题信息分析并撰写以下内容，帮您拓宽课题思路：

AI项目思路

AI技术路线图

贺飞的其他基金

软件合并的安全性问题研究
  • 批准号：
  • 批准年份：
    2020
  • 资助金额：
    57 万元
  • 项目类别：
    面上项目
基于归纳不变式的模型检测研究
  • 批准号：
    61272001
  • 批准年份：
    2012
  • 资助金额：
    61.0 万元
  • 项目类别：
    面上项目
基于假设/保证自动推理的组合验证研究
  • 批准号：
    60903030
  • 批准年份：
    2009
  • 资助金额：
    17.0 万元
  • 项目类别：
    青年科学基金项目

相似国自然基金

{{ item.name }}
  • 批准号：
    {{ item.ratify_no }}
  • 批准年份：
    {{ item.approval_year }}
  • 资助金额：
    {{ item.support_num }}
  • 项目类别：
    {{ item.project_type }}

相似海外基金

{{ item.name }}
{{ item.translate_name }}
  • 批准号：
    {{ item.ratify_no }}
  • 财政年份：
    {{ item.approval_year }}
  • 资助金额：
    {{ item.support_num }}
  • 项目类别：
    {{ item.project_type }}
{{ showInfoDetail.title }}

作者：{{ showInfoDetail.author }}

知道了

AI项目解读示例

课题项目：调控A型流感病毒诱导IFN-β表达的机制研究

AI项目摘要：

本研究聚焦于TRIM2蛋白在A型流感病毒诱导的IFN-β表达中的调控机制。A型流感病毒是全球性健康问题，其感染可导致严重的呼吸道疾病。IFN-β作为关键的抗病毒因子，其表达水平对抗病毒防御至关重要。然而，TRIM2如何调控IFN-β的表达尚未明确。本研究假设TRIM2通过与病毒RNA或宿主因子相互作用，影响IFN-β的产生。我们将采用分子生物学、细胞生物学和免疫学方法，探索TRIM2与A型流感病毒诱导IFN-β表达的关系。预期结果将揭示TRIM2在抗病毒免疫反应中的作用，为开发新的抗病毒策略提供理论基础。该研究对理解宿主抗病毒机制具有重要科学意义，并可能对临床治疗流感病毒感染提供新的视角。

AI项目思路：

科学问题：TRIM2如何调控A型流感病毒诱导的IFN-β表达？
前期研究：已有研究表明TRIM2参与抗病毒反应，但其具体机制尚不明确。
研究创新点：本研究将深入探讨TRIM2在IFN-β表达中的直接作用机制。
技术路线：包括病毒学、分子生物学、细胞培养和免疫检测技术。
关键技术：TRIM2与病毒RNA的相互作用分析，IFN-β启动子活性检测。
实验模型：使用A型流感病毒感染的细胞模型进行研究。

AI技术路线图

        graph TD
          A[研究起始] --> B[文献回顾与假设提出]
          B --> C[实验设计与方法学准备]
          C --> D[A型流感病毒感染模型建立]
          D --> E[TRIM2与病毒RNA相互作用分析]
          E --> F[TRIM2对IFN-β启动子活性的影响]
          F --> G[IFN-β表达水平测定]
          G --> H[TRIM2功能丧失与获得研究]
          H --> I[数据收集与分析]
          I --> J[结果解释与科学验证]
          J --> K[研究结论与未来方向]
          K --> L[研究结束]
关闭
close
客服二维码