嵌入式软件正确性自动证明理论研究

基本信息
批准号:60553002
项目类别:专项基金项目
资助金额:23.00
负责人:顾明
学科分类:
依托单位:清华大学
批准年份:2005
结题年份:2008
起止时间:2006-01-01 - 2008-12-31
项目状态: 已结题
项目参与者:宋晓宇,郭陟,贺飞,万海,张荷花,王睿
关键词:
软件可靠性逻辑验证模型嵌入式软件系统形式化描述及验证
结项摘要

嵌入式系统已经成为现代信息产业中重要和不可缺少的组成部分。随着嵌入式系统复杂性的日益增加,设计出错的可能性也持续增加。对于一个嵌入式系统,花费在验证上的时间是花费在设计上时间的60%。如何有效保证设计的正确性是任何重大系统开发过程中所面临的重要挑战。形式化证明技术是保证系统正确性的一种强有力的方法。形式化证明技术是基于严格数学理论的证明理论与方法,它可以弥补传统模拟的不足。状态爆炸问题是有限状态机

项目摘要

项目成果
{{index+1}}

{{i.achievement_title}}

{{i.achievement_title}}

DOI:{{i.doi}}
发表时间:{{i.publish_year}}

暂无此项成果

数据更新时间:2023-05-31

其他相关文献

1

基于分形L系统的水稻根系建模方法研究

基于分形L系统的水稻根系建模方法研究

DOI:10.13836/j.jjau.2020047
发表时间:2020
2

粗颗粒土的静止土压力系数非线性分析与计算方法

粗颗粒土的静止土压力系数非线性分析与计算方法

DOI:10.16285/j.rsm.2019.1280
发表时间:2019
3

拥堵路网交通流均衡分配模型

拥堵路网交通流均衡分配模型

DOI:10.11918/j.issn.0367-6234.201804030
发表时间:2019
4

中国参与全球价值链的环境效应分析

中国参与全球价值链的环境效应分析

DOI:10.12062/cpre.20181019
发表时间:2019
5

卫生系统韧性研究概况及其展望

卫生系统韧性研究概况及其展望

DOI:10.16506/j.1009-6639.2018.11.016
发表时间:2018

顾明的其他基金

批准号:91018015
批准年份:2010
资助金额:50.00
项目类别:重大研究计划
批准号:90715040
批准年份:2007
资助金额:200.00
项目类别:重大研究计划
批准号:50178049
批准年份:2001
资助金额:22.00
项目类别:面上项目
批准号:91015002
批准年份:2010
资助金额:50.00
项目类别:重大研究计划
批准号:51404236
批准年份:2014
资助金额:25.00
项目类别:青年科学基金项目
批准号:90718039
批准年份:2007
资助金额:250.00
项目类别:重大研究计划
批准号:81803598
批准年份:2018
资助金额:21.00
项目类别:青年科学基金项目

相似国自然基金

1

基于定理证明的可信嵌入式软件建模与验证平台研究

批准号:90718039
批准年份:2007
负责人:顾明
学科分类:F0202
资助金额:250.00
项目类别:重大研究计划
2

构建高可信软件中的自动定理证明问题研究

批准号:61003043
批准年份:2010
负责人:李兆鹏
学科分类:F0203
资助金额:18.00
项目类别:青年科学基金项目
3

复杂程序正确性机器辅助证明的研究

批准号:60373068
批准年份:2003
负责人:张兴元
学科分类:F0203
资助金额:20.00
项目类别:面上项目
4

代数计算及定理机器证明的理论研究与软件开发

批准号:68973030
批准年份:1989
负责人:李廉
学科分类:F0214
资助金额:3.50
项目类别:面上项目