模型检验技术
李
宣
东
李
宣
东
南京大学计算机科学与技术系
提纲
• 软件可信性
• 形式化方法
• 模型检验概述
•
软件系统的模型检验
软件系统的模型检验
•
实时和混成系统的模型检验
•
实时和混成系统的模型检验
研究背景：提高软件可信性
• 随着计算机技术在各行各业应用的日益普及,
计算机已经渗透到我们工作和生活的方方面
计算机已经渗透到我们工作和生活的方方面
面，成为我们工作和生活的一部分，从而极
大地促进了社会的发展和生产力的提高。
• 与此同时，工作在我们身边的各种计算机系
统由于其中的软件系统失效经常表现不尽人
统由于其中的软件系统失效经常表现不尽人
意，呈现出脆弱、难以信任的特征，甚至造
成不可挽回的损失，因此研究相关的可信软
件关键技术以提高软件系统的可信性已经成
为十分迫切的需求。
欧洲阿丽亚娜
型火箭
欧洲阿丽亚娜
5
型火箭
1996年6月4日
因软件失效在
因软件失效在
发射40秒后爆
炸
原因是惯
炸
，
原因是惯
性参考系统
软件的数据
软件的数据
转换异常造
成的失效
成的失效
。
美国
22
猛禽战斗机
美国
F-
22
猛禽战斗机
2007年2月9
日同样因软
件问题延迟
在日本部署
2004
年
12
月
20
日
美空军第
422
测试评估大队的
2004
年
12
月
20
日
，
美空军第
422
测试评估大队的
一
架F-22战斗机因软件问题在起飞过程中失控坠毁。
- 1
- 2
前往页