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

A Microkernel Operating System Program Verification Methods based on UPPAAL

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

With the aerospace, aviation industry＇s development, the credibility verification for airborne embedded software is a software quality problem drawing more and more attention. As formal method is based on rigorous mathematics, we can use it to build an accurate model, describe and verify the software system and we can use this method to find some potential software design faults in the early period. Formal method is an important method to ensure the credibility and safety of airborne software. We use formal verification to analyze and verify some properties in oMer to judge whether the system satisfies these properties. Formal verification can be divided into theorem proving and model checking. This paper mainly includes： study how to use model checking to verify program correctness, propose verification scheme based on model checking, and give a simple case study to show how to use the scheme in the verification. Then finish the procedure in tool UPPAAL.