专利检索 ap:("浙江大学嘉兴研究院" OR "嘉兴天核科技有限公司") AND inv:"谭兴" 第 1 页

1.

发明公开
符合ARINC653标准的操作系统形式化验证方法审中-实审

公开(公告)号：CN117271317A

公开(公告)日：2023-12-22

申请号：CN202311168403.2

申请日：2023-09-11

申请人： 浙江大学嘉兴研究院 , 嘉兴天核科技有限公司

发明人： 赵永望 , 谭兴 , 王布阳 , 任奎 , 张峰

IPC分类号： G06F11/36

摘要： 本发明公开了一种符合ARINC653标准的操作系统形式化验证方法，包括：建立目标操作系统的形式化模型：基于所要验证的操作系统的源代码，使用python语言和z3库函数构建系统的数据结构、类函数，修改所述源代码中的服务函数，向所有服务函数中添加相应的符号执行操作以模拟系统状态变迁过程，从而完成整个操作系统的形式化建模；规范性质验证：基于ARINC653标准得到所有服务的前提条件和预期结果，并将其转换为形式化语言，在步骤(1)得到的形式化模型中调用z3求解器并将转换后的服务的前提条件和预期结果加入z3求解器中，根据求解结果验证系统是否满足相应的规范性质。