嵌入式控制软件的形式化规格说明构建的工程方法

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

基本信息

  • 批准号：
    61402178
  • 项目类别：
    青年科学基金项目
  • 资助金额：
    24.0万
  • 负责人：
    缪炜恺
  • 依托单位：
    华东师范大学
  • 学科分类：
    F0201.计算机科学的基础理论
  • 结题年份：
    2017
  • 批准年份：
    2014
  • 项目状态：
    已结题
  • 起止时间：
    2015-01-01 至2017-12-31

项目摘要

The application of formal methods to industry embedded control software development is not adequately effective as people expected. To tackle this challenge, this project focuses on an engineering method for constructing formal specification of embedded control software. We establish an engineering process for formal specification construction and offer specification review and testing technologies to ensure the consistency and validity of the formal specification. Specifically, our research includes following issues: providing graphic notations with consistent formal semantics for the SPARDL formal specification language; establishing a diagram guided engineering process for formal specification construction to guide the developer construct formal specification from the scratch via particular modeling phases; developing a set of specification review and testing techniques to ensure the consistency and validity of specification; exploring test case generation, animation of testing and test result analysis techniques. We also develop software tools to support our proposed engineering method. This research will enrich both formal modeling theories and methods, and provide industry practitioners with an effective and practical engineering method for formal specification construction. It is also of great significance to quality of embedded control software. The research results can effectively promote the application of formal methods in industry software development.
针对形式化方法在工业界嵌入式控制软件开发过程中难以有效应用的问题，本课题主要研究嵌入式控制软件的形式化规格说明构建工程方法，建立工程化形式化规格说明构建过程，并通过规格说明审查和测试保障规格说明的一致性和有效性。主要研究内容包括：为嵌入式控制软件形式化规格说明语言SPARDL提供与形式化语义一致的图形化描述；建立图形化描述引导的形式化规格说明工程化构建过程，引导开发者从原始需求出发通过不同阶段构建形式化规格说明；研究规格说明审查以保证规格说明的一致性；研究规格说明测试技术以保证规格说明的有效性。研究测试用例生成、测试过程动画模拟及测试结果分析等方法；开发相应的软件工具。课题将丰富当前的形式化建模理论与方法，为工业界嵌入式控制软件的开发者提供有效而实用的形式化规格说明构建工程方法。该课题对提高嵌入式控制软件的质量有重要意义，研究成果可有效推动形式化方法在工业界嵌入式控制软件开发中的实际应用。

结项摘要

在当前的工业界嵌入式控制软件开发领域，形式化方法的实际应用仍面临许多现实困难。从软件需求分析角度看，存在如下主要问题：1)缺乏面向领域的合适的形式化建模语言。2)缺乏系统化的形式化规格说明构建的工程方法。3) 形式化规格说明有效性(validity)检测手段不完善,效率低，缺乏实用的手段。.面对这一挑战，我们提出一种构造嵌入式控制软件形式规格说明的形式工程方法。受国家自然科学基金青年基金资助，课题执行期间取得了如下研究成果：1）提出了一种面向嵌入式控制软件需求建模的轻量级形式化建模语言；2）结合形式化工程方法，建立了一种演化式的形式化模型构建方法，提高了形式化建模过程的效率；3）提出了一种基于图形的需求审查方法，有效地提升了需求审查的错误探测能力；4）提出了一种基于场景的需求模型测试方法，支持在需求分析阶段即可进行仿真分析；5）研发了面向轨道交通车辆控制软件的需求建模工具，使得该方法在企业获得直接应用，显示了该方法具有明确的工程应用价值。

项目成果

期刊论文数量（5）
专著数量（0）
科研奖励数量（0）
会议论文数量（6）
专利数量（0）
An Evolutionary Method for the Formal Specification Construction of Service-based Software
服务型软件形式化规范构建的进化方法
  • DOI：
    --
  • 发表时间：
    2016
  • 期刊：
    International Journal of Software Engineering and Knowledge Engineering
  • 影响因子：
    0.9
  • 作者：
    Weikai Miao;Xi Wang
  • 通讯作者：
    Xi Wang
基于通信的列车控制系统可信构造:形式化方法综述
  • DOI：
    --
  • 发表时间：
    2017
  • 期刊：
    软件学报
  • 影响因子：
    --
  • 作者：
    陈铭松;鲍勇翔;孙海英;缪炜恺;陈小红;周庭梁
  • 通讯作者：
    周庭梁
A Survey on Data Flow Testing
数据流测试综述
  • DOI：
    10.4236/jmf.2013.32a001
  • 发表时间：
    2017
  • 期刊：
    ACM Computing Surveys
  • 影响因子：
    16.6
  • 作者：
    Ting Su;Ke Wu;Weikai Miao;Geguang Pu;Jifeng He
  • 通讯作者：
    Jifeng He
An Automated Test Case Generation Approach based on Activity Diagrams of SysML
基于SysML活动图的自动测试用例生成方法
  • DOI：
    10.23940/ijpe.17.06.p13.922936
  • 发表时间：
    2017
  • 期刊：
    International Journal of Performability Engineering
  • 影响因子：
    --
  • 作者：
    Yufei Yin;Yiqun Xu;Weikai Miao;Yixiang Chen
  • 通讯作者：
    Yixiang Chen
Automated coverage-driven testing: combining symbolic execution and model checking
自动化覆盖驱动测试：结合符号执行和模型检查
  • DOI：
    10.1007/s11432-016-5589-6
  • 发表时间：
    2016
  • 期刊：
    SCIENCE CHINA Information Sciences
  • 影响因子：
    --
  • 作者：
    Ting Su;Geguang Pu;Weikai Miao;Jifeng He;Zhendong Su
  • 通讯作者：
    Zhendong Su

数据更新时间：{{ 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：
    --
  • 发表时间：
    --
  • 期刊：
    软件学报
  • 影响因子：
    --
  • 作者：
    孙海英;缪炜恺;陈小红;周庭梁
  • 通讯作者：
    周庭梁
一种面向列车车载控制软件的需求分析方法
  • DOI：
    10.3969/j.issn.1000-3428.2017.07.008
  • 发表时间：
    2017
  • 期刊：
    计 算 机 工 程
  • 影响因子：
    --
  • 作者：
    王秀超;缪炜恺;王以松;包丹珠;杨静
  • 通讯作者：
    杨静
基于通信的列车控制系统可信构造:形式化方法研究
  • 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技术路线图

缪炜恺的其他基金

基于仿真的嵌入式控制软件设计模型与需求模型之间一致性分析方法
  • 批准号：
    62372181
  • 批准年份：
    2023
  • 资助金额：
    50 万元
  • 项目类别：
    面上项目
数据驱动的机器学习软件系统的形式化需求建模工程方法
  • 批准号：
    61872144
  • 批准年份：
    2018
  • 资助金额：
    64.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
客服二维码