位置：立项数据库 > 立项详情页
基于定理证明的可信嵌入式软件建模与验证平台研究
  • 项目名称：基于定理证明的可信嵌入式软件建模与验证平台研究
  • 项目类别：重大研究计划
  • 批准号：90718039
  • 申请代码：F0202
  • 项目来源：国家自然科学基金
  • 研究期限：2008-01-01-2010-12-01
  • 项目负责人：顾明
  • 负责人职称：研究员
  • 依托单位：清华大学
  • 批准年度：2007
中文摘要：

随着信息技术的发展，嵌入式系统在众多行业中得到广泛使用。为了避免由于嵌入式软件系统本身缺陷或系统中微小的错误而导致系统整体崩溃，嵌入式软件系统的可信性得到了广泛关注。本课题的目标是以定理证明为框架，结合模型检测方法，针对嵌入式软件自身特性，构建基于定理证明的可信嵌入式软件设计过程中建模与验证平台，实现系统级可信属性的验证。为此，本课题拟开展嵌入式软件建模理论及说明语言、基于组合验证的模型分解技术、

中文主题词： 嵌入式软件；软件可信性；定理证明；模型检测
成果综合统计
成果类型
数量
  • 期刊论文
  • 会议论文
  • 专利
  • 获奖
  • 著作
  • 16
  • 24
  • 0
  • 0
  • 1
期刊论文
A deadlock-free scheduling with sequence-dependent setup times
基于Verics的组合Web服务有界模型检测
Integrating Evolutionary Computation with Abstraction Refinement for Model Checking
Specifying and Verifying PLC systems with TLA+: a case study
Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connect
Modeling job shop scheduling with batches and setup times by timed Petri nets
Formalization and Veri?cation of PLC Timers in Coq
Competent Predicate Abstraction in Model Checking
Equality detection for line arithmetic constraints
Formal Modeling and Synthesis of Programmable Logic Controllers
Maxterm Covering for Satisfiability
一种求解认知难题的模型检测方法
COQ定理证明器辅助PLC程序验证和分析
会议论文
Effective Predicate Abstraction for Program Verification
Modeling and Analysis of Real-life Job Shop Scheduling Problems by Petri nets
Modeling and Analysis of Stage Machinery Control Systems by Timed Colored Petri Nets
Formal specification and Code Generation of Programmable Logic Controllers
SimSoC: A full system simulation software for embedded systems
Translation-based model checking for PLC programs
Coq Modulo Theory - Short Paper
Formal Modeling and Verification of Services Managements for Pervasive Computing Environment
A Refinement-Based Validation Method for Programmable Logic Controllers
Parameterized Specification and Verification of PLC Systems in Coq
On Array Theory of Bounded Elements
Verifying Programmable Logic Controllers with Abstraction
A Maximum Weight Heuristic Method for Abstract State Computation
Formalization and Verfication of PLC Timers in Coq
Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning
Compositional Abstraction Refinement for Timed Systems
A Computability Path Ordering for Polymorphic Terms
Specifying time-sensitive systems with TLA+
Data Mining Based Decomposition for Assume-Guarantee Reasoning
Certification of SAT of Solvers in Coq
The Testing Approach of Embedded Real-Time Automatic Control Software Based on Control Objects
Specifying and Verifying PLC systems with TLA+
On the relation between sized-types based termination and semantic labelling
A Computability Path Ordering for Polymorphic Terms - Short Paper
著作
交互式定理证明与程序开发
相关项目
安全协议的行为时序逻辑验证与具有公平性约束的部分状态空间模型检测
期刊论文 16 会议论文 4
航天嵌入式软件可信性保障集成环境和示范验证与应用
期刊论文 86 会议论文 82
面向目标的语义Web服务测试
期刊论文 8 会议论文 11
基于约束凸多面体和抽象加细技术的混合系统的模型检测
期刊论文 22 会议论文 4 专利 1
基于一阶符号轨迹计算理论的模型检测
期刊论文 5 会议论文 11
基于抽象的软件符号模型检测研究
期刊论文 20
符号轨迹计值的形式化语义及模型检测技术研究
期刊论文 1 会议论文 3
面向对象程序的形式化规范与验证
期刊论文 4 会议论文 14
物联网中可信设备协同的建模与验证方法研究
期刊论文 5 会议论文 9
顾明的项目
基于多物理信号的高速列车系统级健康分析仪器
面向领域的可信嵌入式软件系统试验验证环境研究
期刊论文 5 会议论文 7
可信嵌入式软件系统试验环境与示范应用
期刊论文 28
嵌入式软件正确性自动证明理论研究
嵌入式系统仿真与验证平台开发
期刊论文 1
中国建筑信息化技术发展战略研究
期刊论文 5
基于轨道车辆视频监测数据的快速异常检测技术研究
期刊论文 3 会议论文 3