嵌入式多核操作系统的形式化建模与验证  

Formal Model and Verification of Safety- critical Software

作　　者：郝继锋[1] 胡宁[1] 任晓瑞[1] 周霆[1] HAO Ji-feng;HU Ning;REN Xiao-rui;ZHUO Ting(Xi′an Aeronautics Computing Technique Research Institute,AVIC,Xi′an 710000,China)

机构地区：[1]航空工业西安航空计算技术研究所,陕西西安710000

出　　处：《航空计算技术》2022年第6期124-128,共5页Aeronautical Computing Technique

基　　金：国家自然科学基金项目资助(61732001)。

摘　　要：在安全关键系统中,核心基础软件的正确性尤其重要。任何的错误都可能导致整体系统失效,带来严重的后果,同时,安全关键软件要通过高等级国际安全认证标准,则必须使用形式化方法进行设计、建模和验证。调研嵌入式操作系统、编译器、文件系统、机载网络/总线的形式化验证案例,在此基础之上引出嵌入式多核操作系统形式化的问题;对嵌入式多核操作系统的时间确定性和功能正确性属性进行形式化建模和验证;并对全文进行总结。The Safety-critical software must use formal methods because of the safety certification requirement.Firstly,the paper investigates the formal verification cases of embedded operating system,compiler,file system and avionics network/bus,then the formal verification of embedded multicore operating system is introduced;Secondly,we model and verify the time determinism and functional correctness attributes of embedded multicore operating system formally.Finally,the pros and cons of formal methods using in engineering are summarized.

关 键 词：安全关键软件 安全认证 形式化方法 嵌入式多核操作系统 时间确定性 功能正确性 形式化建模和验证 

分 类 号：TP316.2[自动化与计算机技术—计算机软件与理论]