PAR平台中算法程序模型变换正确性研究

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

基本信息

  • 批准号：
    61662036
  • 项目类别：
    地区科学基金项目
  • 资助金额：
    39.0万
  • 负责人：
    胡启敏
  • 依托单位：
    江西师范大学
  • 学科分类：
    F0201.计算机科学的基础理论
  • 结题年份：
    2020
  • 批准年份：
    2016
  • 项目状态：
    已结题
  • 起止时间：
    2017-01-01 至2020-12-31

项目摘要

PAR platform was software formal and automate development platform which was developed by our research team by more than twenty years of independent research and support of national research projects. PAR implemented MDD by transform Radl model to Apla model, and Apla model to executeable program model. This project will research on correctness of model tranformation in PAR platform, especially Apla model to executeable program model. The research content include verficating Apla model by Isabelle and Loop invariants semi-automatically, verifacting generic constraint by algebra structure and axiomatic semantics, ensuring the model transformation of APLA programs to executable program model is correct by generation rules and key transformation algorithm, exploring the correctness of service interaction mechanism in Apla+ model. It is expected that the final solution to ensure the correctness of the model transformation which is a very challenging and creative problem. Along our unique technical route, occupy the international high ground of high reliability software formal and automatic development as soon as possible.
PAR平台是申请者所在团队历经二十多年，在十几项国家级课题连续资助下，自主研发的软件形式化与自动化开发平台。PAR平台通过Radl程序模型变换为Apla程序模型，再变换为可执行程序模型，实现了模型驱动的软件开发。围绕PAR平台中模型变换的正确性，尤其是Apla程序模型到可执行程序模型变换过程中的正确性验证开展深入研究。重点研究利用新策略开发循环不变式，进而通过Isabelle定理证明器半自动验证Apla程序模型的正确性；通过代数结构与公理语义验证Apla程序模型中泛型约束机制的正确性；通过验证生成规则和关键变换算法，保证Apla程序模型变换为可执行程序模型的正确性；并探索Apla+程序模型中服务交互机制正确性验证问题。有望最终解决保证模型变换正确性，这一极具挑战性和创造性的问题。沿着我们特有的技术路线，尽快占领高可靠软件的形式化与自动化开发领域的国际制高点。

结项摘要

PAR平台是申请者所在团队历经二十多年，在十几项国家级课题连续资助下，自主研发的软件形式化与自动化开发平台。PAR平台通过Radl程序模型变换为Apla程序模型，再变换为可执行程序模型，实现了模型驱动的软件开发。.围绕PAR平台中模型变换的正确性，重点研究了利用新策略开发循环不变式，进而通过定理证明器验证Apla程序模型的正确性；验证Apla程序模型中泛型约束机制的正确性；验证Apla程序模型变换为可执行程序模型的正确性；探索Apla+程序模型中服务交互机制正确性的验证。.利用两种开发新策略为Apla程序模型开发循环不变式。结合循环不变式开发新策略取得的研究成果，Hoare公理体系、Dijkstra最弱前置谓词方法和定理证明系统的自身特点，给出用定理证明器机械化验证Apla程序模型正确的方法，并总结了验证的主要步骤。.基于一阶谓词逻辑给出基本数据类型作泛型参数，基于代数结构给出自定义抽象数据类型作泛型参数，基于公理语义给出子程序作泛型参数的约束机制。成功将上述泛型约束机制转变为Isar证明脚本，并利用Isabelle定理证明器对约束机制正确性进行验证，同时完成验证Apla程序模型变换为可执行程序模型的正确性。.成功扩展PAR平台Apla+语言（并发分布和顺序程序设计通用的语言），通过在Apla语言中扩充并行、衍生、顺序、调用和选择等五个服务交互算子，将Apla程序模型过渡到能够实现服务交互机制的Apla+程序模型。在此基础上，建立服务交互的Apla+表示到相关验证工具SMV表示的转换工具，实现服务交互程序模型的验证。.圆满完成研究计划，取得预期研究成果。在学术论文方面，发表学术论文11篇，其中学术期刊论文6篇，国际学术会议论文5篇，EI收录6篇。在学术交流方面，参加国际学术会议11人次，参加国内学术会议19人次，承办学术会议或学术活动3场。在人才培养方面，培养博士研究生2人，青年教师2人，硕士研究生8人。.

项目成果

期刊论文数量（6）
专著数量（0）
科研奖励数量（0）
会议论文数量（5）
专利数量（0）
基于Web Service和多媒体数据库技术的PAR方法在线自学系统的设计与实现
  • DOI：
    10.16357/j.cnki.issn1000-5862.2018.03.12
  • 发表时间：
    2018
  • 期刊：
    江西师范大学学报(自然科学版)
  • 影响因子：
    --
  • 作者：
    熊小舟;薛锦云
  • 通讯作者：
    薛锦云
PAR平台中若干软件构件形式化验证技术研究
  • DOI：
    --
  • 发表时间：
    2018
  • 期刊：
    计算机工程与科学
  • 影响因子：
    --
  • 作者：
    胡启敏;薛锦云;游珍;程着
  • 通讯作者：
    程着
无线射频RFID识别协议自动验证方法研究
  • DOI：
    10.11896/j.issn.1002-137x.2017.09.020
  • 发表时间：
    2017
  • 期刊：
    计算机科学
  • 影响因子：
    --
  • 作者：
    宋岚;薛锦云;胡启敏;谢武平;江东明;游珍
  • 通讯作者：
    游珍
Formal Development of Linear Structure Reusable Components in PAR Platform
PAR平台线性结构可复用组件的正式开发
  • DOI：
    10.1007/978-3-319-57708-1_6
  • 发表时间：
    2017
  • 期刊：
    Lecture Notes in Computer Science
  • 影响因子：
    --
  • 作者：
    Qimin Hu;Jinyun Xue;Zhen You
  • 通讯作者：
    Zhen You
虚拟现实软件系统开发方法研究
  • DOI：
    10.3969/j.issn.1007-130x.2019.11.010
  • 发表时间：
    2019
  • 期刊：
    计算机工程与科学
  • 影响因子：
    --
  • 作者：
    周哲泓;薛锦云;黄捷文
  • 通讯作者：
    黄捷文

数据更新时间：{{ 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 }}

其他文献

无线射频RFID识别协议自动验证方法研究
  • DOI：
    10.1038/s41598-019-44663-9
  • 发表时间：
    2017
  • 期刊：
    计算机科学
  • 影响因子：
    --
  • 作者：
    宋岚;薛锦云;胡启敏;谢武平;江东明;游珍
  • 通讯作者：
    游珍
PAR平台中若干软件构件形式化验证技术研究
  • DOI：
    --
  • 发表时间：
    2018
  • 期刊：
    计算机工程与科学,2018,40(02)
  • 影响因子：
    --
  • 作者：
    胡启敏;薛锦云;游珍
  • 通讯作者：
    游珍
基于Spring框架的轻量级J2EE架构与应用
  • DOI：
    10.1016/j.ijpharm.2021.120364
  • 发表时间：
    --
  • 期刊：
    计算机工程与应用
  • 影响因子：
    --
  • 作者：
    胡启敏;薛锦云
  • 通讯作者：
    薛锦云
PAR平台中若干软件构件形式化验证技术研究
  • DOI：
    --
  • 发表时间：
    2018
  • 期刊：
    计算机工程与科学,2018,40(02)
  • 影响因子：
    --
  • 作者：
    胡启敏;薛锦云;游珍
  • 通讯作者：
    游珍
若干算法程序的形式化推导与生成技术研究
  • DOI：
    --
  • 发表时间：
    --
  • 期刊：
    计算机研究与发展
  • 影响因子：
    --
  • 作者：
    胡启敏;薛锦云
  • 通讯作者：
    薛锦云

其他文献

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

AI项目思路

AI技术路线图

相似国自然基金

{{ 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
客服二维码