Patent search ap:("北京控制工程研究所") AND inv:"马智" Page 1

1.

发明公开
一种嵌入式操作系统设计层形式化验证方法审中-实审

公开(公告)号：CN115185812A

公开(公告)日：2022-10-14

申请号：CN202210641003.8

申请日：2022-06-07

Applicant: 北京控制工程研究所

Inventor： 张锦坤 , 乔磊 , 杨孟飞 , 杨桦 , 刘波 , 马智

IPC: G06F11/36

Abstract: 一种嵌入式操作系统设计层形式化验证方法，首先，从操作系统详细设计报告中，获取操作系统包含的函数模块、各函数模块的具体功能及流程图，提炼操作系统各函数模块应满足的局部性质；构建操作系统的系统状态及确立引起系统状态变化的触发事件；然后建立基于有限状态机的操作系统设计层形式化模型；在定理证明器Coq中将局部性质和操作系统设计层形式化模型进行形式化定义，验证操作系统设计层形式化模型是否满足所述局部性质，若满足，则操作系统设计层正确可靠；若不满足，确定详细设计报告中存在问题的流程图及具体位置。本发明可以准确地描述操作系统的设计过程，以便更早地发现是否有潜在的错误。

Patent Agency Ranking