Formal modeling and verification method for inter-process communication mechanism of microkernel operating system based on Event-B method

Abstract

The invention discloses a formal modeling and verification method for an inter-process communication mechanism of a microkernel operating system based on an Event-B method. The method comprises the steps that demand design analysis is conducted, specifically, according to a microkernel operating system inter-process communication mechanism based on an Event-B method, in combination with a subscriber publisher mode, design analysis is conducted to meet the original demand of Event-B modeling; according to the inter-process communication mechanism of the microkernel operating system based on theEvent-B method and the result of the original demand, designing and analyzing meet the rewriting demand of Event-B modeling; and modeling and refining verification: a model for verifying the inter-process communication mechanism of the microkernel operating system is designed and created based on the Event-B method according to a rewriting demand. Proving obligations needing to be verified by themodel comprise a model functional invariant, a model property invariant and a safety property related invariant.

Description

technical field [0001] The invention belongs to the technical field of micro-kernel operating system modeling and verification, and in particular uses the Event-B modeling verification language to design a method for rewriting requirements and modeling verification of a micro-kernel operating system inter-process communication mechanism based on the Event-B method. Background technique [0002] The operating system is the cornerstone of the Internet era. However, with the continuous development of the times, the macro-kernel operating system is becoming larger and larger. For the sake of execution efficiency and simple architecture, there are a large number of unnecessary functional services in the kernel. This situation makes the macro kernel operating system more and more functions, but also makes its security worse and worse, because the huge code will inevitably lead to some loopholes and conflicts. [0003] The microkernel operating system is different from the macroker...

AI Technical Summary

Problems solved by technology

[0006] The present invention overcomes the difficulty that the inter-process communication mechanism of the micro-kernel operating system is difficult to model, according to the rewritten requirements of the original requirements of the inter-process communication mechanism of the micro-kernel operating system, the micro-kernel operating system environment and the inter-process The communication mechanism establishes an abstract model, refines the model in multiple layers, and finally obtains an implementation model that meets the above requirements, and proves the feasibility and security of the mechanism in the implementation model

Images