首页> 中国专利> 基于Event-B方法的微内核操作系统进程间通信机制的形式化建模和验证方法

基于Event-B方法的微内核操作系统进程间通信机制的形式化建模和验证方法

页面导航

摘要
著录项
法律信息
相似文献

摘要

本发明公开了一种基于Event‑B方法的微内核操作系统进程间通信机制的形式化建模和验证方法，包括：需求设计分析，根据基于Event‑B方法的微内核操作系统进程间通信机制，结合订阅者发布者模式，设计分析符合Event‑B建模的原始需求。根据基于Event‑B方法的微内核操作系统进程间通信机制以及原始需求的结果，设计分析符合Event‑B建模的重写需求；建模精化验证，根据重写需求，设计建立验证基于Event‑B方法的微内核操作系统进程间通信机制的模型。该模型需要验证的证明义务包括模型功能性不变式以及模型性质不变式和安全性质相关不变式。

著录项

公开/公告号CN110968436A

专利类型发明专利
公开/公告日2020-04-07

原文格式PDF
申请/专利权人华东师范大学;
展开▼

申请/专利号CN201911051831.0
发明设计人李钦;关钰千;郭建;蒲戈光;
展开▼

申请日2019-10-31
分类号
代理机构上海麦其知识产权代理事务所(普通合伙);
代理人董红曼
地址 200062 上海市普陀区中山北路3663号
入库时间 2023-12-17 07:08:50

法律信息

法律状态公告日

法律状态信息

法律状态
2020-05-01

实质审查的生效 IPC(主分类):G06F9/54 申请日:20191031

实质审查的生效
2020-04-07

公开

公开

相似文献

专利
中文文献
外文文献

1. 基于Event-B方法的微内核操作系统进程间通信机制的形式化建模和验证方法 [P] . 中国专利： CN110968436A . 2020-04-07
2. 基于边界模型检测技术的微内核操作系统接口的形式化验证方法 [P] . 中国专利： CN111679964A . 2020-09-18
3. FINITE-STATE MACHINE-BASED METHOD AND DEVICE FOR OPERATING SYSTEM REQUIREMENT LAYER FORMAL MODELING [P] . 世界知识产权组织专利： WO2020221097A1 . 2020-11-05

机译：基于有限状态机的操作系统需求层形式化建模方法和装置
4. A method for verifying drones in Industrial Internet of Things using Petri net modeling [P] . 韩国专利： KR102050230B1 . 2019-11-29

机译：基于Petri网建模的工业物联网无人机验证方法
5. Formal methods for modeling and analysis of hybrid systems [P] . 美国专利： US7574334B2 . 2009-08-11

机译：混合系统建模和分析的形式化方法