华东师范大学学报（自然科学版）Issue(4)：1-17,17.DOI:10.3969/j.issn.1000-5641.2024.04.001
一种面向嵌入式操作系统的形式化验证方法
A formal verification method for embedded operating systems
摘要
Abstract
The operating system is the core and foundation of the entire computer system.Its reliability and safety are vital because faults or vulnerabilities in the operating system can lead to system crashes,data loss,privacy breaches,and security attacks.In safety-critical systems,any errors in the operating system can result in significant loss of life and property.Ensuring the safety and reliability of the operating system has always been a major challenge in industry and academia.Currently,methods for verifying the operating system's safety include software testing,static analysis,and formal methods.Formal methods are the most promising in ensuring the operating system's safety and trustworthiness.Mathematical models can be established using formal methods,and the system can be formally analyzed and verified to discover potential errors and vulnerabilities.In the operating system,formal methods can be used to verify the correctness and completeness of the operating system's functions and system safety.A formal scheme for embedded operating systems is proposed herein on the basis of existing formal verification achievements for operating systems.This scheme uses VCC(verified C compiler),CBMC(C bounded model checker),and PAT(process analysis toolkit)tools to verify the operating system at the unit,module,and system levels,respectively.The schema,upon being successfully applied to a task scheduling architecture case of a certain operating system,exhibits a certain universality for analyzing and verifying embedded operating systems.关键词
嵌入式操作系统/形式化验证/VCC/CBMC/PATKey words
embedded operating system/formal verification/VCC/CBMC/PAT分类
信息技术与安全科学引用本文复制引用
王阳,方竟成,蔡雄,张志鹏,蔡喁,缪炜恺..一种面向嵌入式操作系统的形式化验证方法[J].华东师范大学学报（自然科学版）,2024,(4):1-17,17.基金项目
国家自然科学基金(62372181) （62372181）
