面向信息物理融合系统的程序统一理论研究

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

基本信息

  • 批准号：
    61872145
  • 项目类别：
    面上项目
  • 资助金额：
    63.0万
  • 负责人：
    朱惠彪
  • 依托单位：
    华东师范大学
  • 学科分类：
    F0201.计算机科学的基础理论
  • 结题年份：
    2022
  • 批准年份：
    2018
  • 项目状态：
    已结题
  • 起止时间：
    2019-01-01 至2022-12-31

项目摘要

Cyber-Physical System (CPS for short) is a new generation system, which is deeply connected by computing, communication and control, enhancing the ability of physical systems through networked computing. Unifying Theories of Programming (UTP for short) was developed by C.A.R. Hoare (Turing Award Winner) and Jifeng He in 1998, which has been recognized as an outstanding method for various programming. This project is devoted to investigate UTP for CPS, focusing on the mixing of continuous/discrete, time-space consistency, collaboration and networking. The study of this project includes constructing modeling languages for the features of CPS, investigating the denotational semantics, algebra semantics, operational semantics and deduction system, aiming to support the correct description and property verification for CPS. This project also explores the consistency among the four formal models from different viewpoints, ensuring the correctness of the semantical models and deduction system. Based on the theoretical achievements of formal semantics and deduction system, the analysis and verification of typical case studies is also studied. The investigation of this project will make meaningful extensions for UTP and provide theoretical support for the safety of CPS.
信息物理融合系统是计算、通讯和控制深度交联，通过网络化计算增强物理系统能力的新一代系统。程序统一理论是由图灵奖获得者C.A.R. Hoare教授和华东师范大学何积丰院士于1998年提出，已经被国际上公认为研究各类程序的一种优秀的方法。本项目针对信息物理融合系统的连续离散融合、时空一致性、协同性、网络化等特性，致力于面向信息物理融合系统的程序统一理论的研究。为信息物理融合系统的典型特性构建建模语言，研究其指称语义、代数语义、操作语义及证明系统，支持信息物理融合系统精确的行为刻画和性质验证。采用不同的视角研究这四种形式化模型的一致性，为语义模型和证明系统的正确性提供了形式化保证。基于形式语义和证明系统的理论成果，开展信息物理融合系统典型案例的分析验证。本项目的研究将对程序统一理论产生理论意义的拓展，并对信息物理融合系统的安全性提供理论支持。

结项摘要

信息物理融合系统(CPS)是计算、通讯和控制深度交联，通过网络化计算增强物理系统能力的新一代系统。程序统一理论(UTP)是由图灵奖获得者C.A.R. Hoare教授和华东师范大学何积丰院士于1998年提出，已经被国际上公认为研究各类程序的一种优秀的方法。本项目面向若干特定CPS领域，针对建模语言的构造及相应的UTP理论，开展了一系列的研究。. 首先，对于MDESL建模语言，我们从理论和实践两个角度开展了UTP理论的相关研究，主要包括MDESL代数语义和操作语义连接的理论和机械证明，以及MDESL指称语义和代数语义的理论和机械研究。从理论和实践的角度对操作语义的正确性和完备性及代数定律的正确性进行了验证。其中，机械证明和研究都是基于定理证明器Coq完成的。同时，我们构造了移动分布式系统的进程演算BigrTiMo，演算不但捕捉了移动计算的移动性，还刻画了移动计算的空间结构和时间特性，我们开展了其操作语义、指称语义、代数语义、证明系统以及语义连接的研究。此外，传统的CPS系统大多基于通讯进行信息交互，我们构造了基于共享变量的CPS系统建模语言，并研究了其指称语义、代数语义和证明系统。其中，指称语义和证明系统都是基于轨迹模型。针对物联网和移动边缘计算等网络化系统，我们也开展了其UTP语义的研究。最后，我们以车联网为案例开展了CPS系统的验证研究。

项目成果

期刊论文数量（9）
专著数量（0）
科研奖励数量（0）
会议论文数量（16）
专利数量（0）
Theoretical and Practical Aspects of Linking Operational and Algebraic Semantics for MDESL
MDESL 的运算语义和代数语义的理论和实践方面
  • DOI：
    10.1145/3295699
  • 发表时间：
    2019
  • 期刊：
    ACM Transactions on Software Engineering and Methodology
  • 影响因子：
    4.4
  • 作者：
    Feng Sheng;Huibiao Zhu;Jifeng He;Zongyuan Yang;Jonathan P.Bowen
  • 通讯作者：
    Jonathan P.Bowen
Specification and Verification of the Zab Protocol with TLA+
使用 TLA 规范和验证 Zab 协议
  • DOI：
    10.1007/s11390-020-0538-7
  • 发表时间：
    2020
  • 期刊：
    Journal of Computer Science and Technology
  • 影响因子：
    1.9
  • 作者：
    Jiaqi Yin;Huibiao Zhu;Yuan Fei
  • 通讯作者：
    Yuan Fei
Event-based functional decomposition
基于事件的功能分解
  • DOI：
    10.1016/j.ic.2019.104484
  • 发表时间：
    2020
  • 期刊：
    Information and Computation
  • 影响因子：
    1
  • 作者：
    Jian-Min Jiang;Huibiao Zhu;Qin Li;Yongxin Zhao;Shi Zhang;Ping Gong;Zhong Hong
  • 通讯作者：
    Zhong Hong
A process calculus BigrTiMo of mobile systems and its formal semantics
移动系统过程演算BigrTiMo及其形式语义
  • DOI：
    10.1007/s00165-021-00530-x
  • 发表时间：
    2021
  • 期刊：
    FORMAL ASPECTS OF COMPUTING
  • 影响因子：
    1
  • 作者：
    Wanling Xie;Huibiao Zhu;Qiwen Xu
  • 通讯作者：
    Qiwen Xu
Language evolution and healthiness for critical cyber-physical systems
关键网络物理系统的语言演变和健康状况
  • DOI：
    10.1002/smr.2301
  • 发表时间：
    2021
  • 期刊：
    JOURNAL OF SOFTWARE-EVOLUTION AND PROCESS
  • 影响因子：
    --
  • 作者：
    Richard Banach;Huibiao Zhu
  • 通讯作者：
    Huibiao Zhu

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

其他文献

其他文献

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

AI项目思路

AI技术路线图

朱惠彪的其他基金

Web事务的模型和语义研究
  • 批准号：
    90718004
  • 批准年份：
    2007
  • 资助金额：
    50.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
客服二维码