多类型时序逻辑程序设计

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

基本信息

  • 批准号：
    61402347
  • 项目类别：
    青年科学基金项目
  • 资助金额：
    26.0万
  • 负责人：
    赵亮
  • 依托单位：
    西安电子科技大学
  • 学科分类：
    F0201.计算机科学的基础理论
  • 结题年份：
    2017
  • 批准年份：
    2014
  • 项目状态：
    已结题
  • 起止时间：
    2015-01-01 至2017-12-31

项目摘要

Temporal logic programming is currently one of the most widely used programming paradigms, and it has great significance for program verification. This project proposes research on many-type temporal logic programming, so as to enhance temporal logic programming in its functionality and applicability. For this, we propose to introduce the notion of type and define multiple types on the basis of Modelling, Simulation and Verification Language (MSVL), obtaining Many-Type MSVL, a many-type temporal logic programming language. We plan to study its type system, model semantics, operational semantics, axiomatic semantics, type safety, and equivalence between different semantics. In addition, we are going to develop an interpreter for Many-Type MSVL, implementing the type checking, modelling, simulation and verification of many-type temporal logic programs.
时序逻辑程序设计是目前一种广泛使用的程序设计模式，对程序验证具有重要的意义。本项目拟研究多类型时序逻辑程序设计，以加强时序逻辑程序设计的功能和适用性。为此，我们在建模、仿真和验证语言（MSVL）的基础上引入类型的概念，并定义多种类型，得到一种多类型时序逻辑程序设计语言：多类型MSVL。研究多类型MSVL的类型系统、模型语义、操作语义、公理语义、类型安全性和语义之间等价性。开发多类型MSVL的解释器，实现对多类型时序逻辑程序的类型检查、建模、仿真和验证。

结项摘要

时序逻辑程序设计是目前一种广泛使用的程序设计模式，对程序验证具有重要的意义。现有的时序逻辑程序设计语言注重在逻辑方面的功能，然而在类型方面的功能有限，往往仅支持单一类型。本项目对建模、仿真和验证语言MSVL进行扩展，使用投影时序逻辑PTL定义了整型、浮点型、字符型、数组、列表、指针、结构等多种类型以及各类型的相关操作，得到了一种多类型的时序逻辑程序设计语言。构建了多类型MSVL的形式语义理论体系，以极小模型的方式定义了该语言的模型语义，以格局约简的方式定义了该语言的操作语义，并证明了这两种语义的等价性。研究了基于PTL的程序验证理论，提出了相应的模型检测方法和运行时验证方法。作为理论的实现，开发出多类型MSVL的解释器工具，具备对多类型时序逻辑程序的建模、仿真与验证功能。作为理论和工具的应用，实现了一种基于多类型MSVL的社交网络系统验证方法，并使用该方法验证了社交网络系统中若干条关于隐私策略和用户关系强度的性质。本项目对多类型MSVL的开发与研究改进了目前国内外时序逻辑程序设计语言缺乏多类型支持这一不足，增强了时序逻辑程序设计的功能和适用性。

项目成果

期刊论文数量（3）
专著数量（0）
科研奖励数量（1）
会议论文数量（3）
专利数量（5）
A compiler for MSVL and its applications
MSVL编译器及其应用
  • DOI：
    10.1016/j.tcs.2017.07.032
  • 发表时间：
    2017-08
  • 期刊：
    Theoretical Computer Science
  • 影响因子：
    1.1
  • 作者：
    Kai Yang;Zhenhua Duan;Cong Tian;Nan Zhang
  • 通讯作者：
    Nan Zhang
Model Checking of Pushdown Systems for Projection Temporal Logic
投影时态逻辑下推系统的模型检验
  • DOI：
    10.1016/j.tcs.2016.06.031
  • 发表时间：
    --
  • 期刊：
    Theoretical Computer Science
  • 影响因子：
    1.1
  • 作者：
    Liang Zhao;Xiaobing Wang;Zhenhua Duan
  • 通讯作者：
    Zhenhua Duan

数据更新时间：{{ 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.14042/j.cnki.32.1309.2016.04.015
  • 发表时间：
    2016
  • 期刊：
    水科学进展
  • 影响因子：
    --
  • 作者：
    张巍;赵亮;贺治国;林挺;谈利明;蒋后硕
  • 通讯作者：
    蒋后硕
考虑驱动和负载状态的三自由度超声电机接触模型研究
  • DOI：
    10.13465/j.cnki.jvs.2021.03.023
  • 发表时间：
    2021
  • 期刊：
    振动与冲击
  • 影响因子：
    --
  • 作者：
    李争;赵亮;郭鹏;于絮泽
  • 通讯作者：
    于絮泽
PTAOD: A Novel Framework for Supporting Approximate Outlier Detection Over Streaming Data for Edge Computing
PTAOD：一种支持边缘计算流数据近似异常值检测的新型框架
  • DOI：
    10.1109/access.2019.2962066
  • 发表时间：
    2020
  • 期刊：
    IEEE ACCESS
  • 影响因子：
    3.9
  • 作者：
    朱睿;于甜甜;谭志远;杜威;赵亮;李佳佳;夏秀峰
  • 通讯作者：
    夏秀峰
Local Minimum Energy of LBP Algorithm Concrete CT Image Segmentation
LBP算法混凝土CT图像分割的局部最小能量
  • DOI：
    10.14257/ijsip.2014.7.4.17
  • 发表时间：
    2014-08
  • 期刊：
    International Journal of Signal Processing, Image Processing and Pattern Recognition
  • 影响因子：
    --
  • 作者：
    赵亮;鲁君;徐胜军
  • 通讯作者：
    徐胜军
基于Ergun方程的菱镁球团填充床层阻力特性实验
  • DOI：
    10.12068/j.issn.1005-3026.2021.03.007
  • 发表时间：
    2021
  • 期刊：
    东北大学学报. 自然科学版
  • 影响因子：
    --
  • 作者：
    张晟;张晓虎;赵亮;董辉
  • 通讯作者：
    董辉

其他文献

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

AI项目思路

AI技术路线图

赵亮的其他基金

神经网络系统的形式化建模与验证
  • 批准号：
    61972301
  • 批准年份：
    2019
  • 资助金额：
    60 万元
  • 项目类别：
    面上项目

相似国自然基金

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