位置：立项数据库 > 立项详情页
面向领域的可信嵌入式软件系统试验验证环境研究
  • 项目名称：面向领域的可信嵌入式软件系统试验验证环境研究
  • 项目类别：重大研究计划
  • 批准号：91018015
  • 申请代码：F020106
  • 项目来源：国家自然科学基金
  • 研究期限：2011-01-01-2011-12-31
  • 项目负责人：顾明
  • 负责人职称：研究员
  • 依托单位：清华大学
  • 批准年度：2010
中文摘要：

软件可信性是系统层次的概念，如何对现有专注于软件开发生命周期某一阶段的传统方法和技术进行有效集成，形成对软件可信性的整体评估，是目前亟待解决的问题。此外，软件可信性评估与领域紧密相关，应用于不同领域的软件系统因其自身固有特性，在软件可信性评估上具有不同的侧重点。本课题以嵌入式软件系统为应用载体，研究面向特定领域的软件可信建模验证方法与技术，基于领域知识有效抽取可信需求、降低可信建模难度和提高可信验证有效性。研究设计和开发能够将可信需求描述、软件行为建模以及可信验证等各阶段有效综合的集成建模验证工具，并在典型嵌入式软件系统案例上进行检验，展示研究成果的集成效果。

中文主题词： 领域知识，可信基准线，领域建模语言，形式验证，嵌入式软件
成果综合统计
成果类型
数量
  • 期刊论文
  • 会议论文
  • 专利
  • 获奖
  • 著作
  • 5
  • 7
  • 0
  • 0
  • 0
期刊论文
The Denotational Semantics Definition of PLC Programs Based on Extended λ-Calculus.
New strategies for reliability analysis of Programmable Logic Controllers
一种PLC程序语言指称语义及函数的形式化定义方法
Semantic Characterization of Programmable Logic Controller Programs
基于BIP框架的DPU系统建模与验证
会议论文
The Verification of PLC Program Based on Interactive Theorem Proving Tool COQ
CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decid
An Efficient Resolution Based Algorithm for SAT
Proving Computational Geometry Algorithms in TLA+2
Edola: the domain modeling and verification language for PLC systems
Modeling and Validation of a Data Process Unit Control for Space Applications
Domain-driven Probabilistic Analysis of Programmable Logic Controllers
相关项目
高可信嵌入式软件系统典型案例研究及试验验证环境设计
期刊论文 1 会议论文 1
基于领域知识的肝脏CT图割模型研究
期刊论文 11 会议论文 11
航天嵌入式软件可信性保障集成环境和示范验证与应用
期刊论文 86 会议论文 82
从行为级到版图级的设计验证与测试生成
期刊论文 133 会议论文 48
领域知识驱动的深层知识发现研究
期刊论文 25 会议论文 14 获奖 8
基于领域知识的主题分析和文本结构分析技术研究
期刊论文 14 会议论文 31 获奖 2
可信网络软件的形式验证
期刊论文 32 会议论文 22 专利 1 著作 1
支持协同产品开发的领域知识处理方法研究
期刊论文 9 会议论文 10
大规模时空数据集的高效知识发现核心问题研究
期刊论文 18 会议论文 3
顾明的项目
基于定理证明的可信嵌入式软件建模与验证平台研究
期刊论文 16 会议论文 24 著作 1
中国建筑信息化技术发展战略研究
期刊论文 5
基于轨道车辆视频监测数据的快速异常检测技术研究
期刊论文 3 会议论文 3
基于多物理信号的高速列车系统级健康分析仪器
可信嵌入式软件系统试验环境与示范应用
期刊论文 28
嵌入式软件正确性自动证明理论研究
嵌入式系统仿真与验证平台开发
期刊论文 1