基于UPPAAL的微内核操作系统程序验证方法研究

• 作者: 杨达
• 来源期刊: 电脑与信息技术
• 学科: 工学
• 关键词: 微内核操作系统 形式化方法 模型检测
• 年，卷（期）: 2014,（5）
• 所属期刊栏目: 人工智能与算法研究
• 页码范围: 24-26,66
• 页数: 4页
• 分类号: TP316.2
• 字数: 2541字
• 语种: 中文

摘要

随着航天、航空工业的发展,机载嵌入式软件的可信属性验证是新一代飞机研制最关注的软件质量保障问题.形式化方法具有严密的数学基础,能够准确的对系统进行建模、描述和验证,能够在软件系统的设计初期发现潜在的错误,是保证机载软件可信性和安全性的软件正确性验证技术.形式化验证以形式化描述为基础,对所描述系统的特性进行分析和验证,以评判系统是否满足期望的性质,分为定理证明和模型检测两类.文章研究模型检测方法应用于程序形式化描述和验证的技术,提出基于模型检测的验证程序正确性的方案,并进行微内核操作系统程序分析,最后在UPPAAL中进行程序属性的验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨达		2	0	0.0	0.0