| The Event-B method is a formal approach proposed in the computer field for system level modeling and analysis.It evolved from Method B,where the static model context and dynamic model machine of Method B are integrated in the same file with high coupling.The Event-B method inherits and extends Method B,extracting the context from the machine and introducing events into the machine,making it more suitable for periodic modeling processes,making the model clearer and reducing the occurrence of errors.The two important characteristics of the Event-B method are layer by layer refinement and ambiguity free.Complex software systems can be split through the layer by layer refinement of the Event-B method,reducing the difficulty of system modeling;Key software systems can be mathematically modeled through the ambiguity free nature of Event-B to ensure system correctness.The immune system is a medium-sized complex software system,and the elevator system is a medium-sized key software system.This project will focus on the immune system and elevator system as research objects,and focus on the application of Event-B method in modeling complex software systems and key software systems,exploring the solutions provided by Event-B method in responding to different software requirements.The main research content of this project mainly includes using Event-B to formalize and validate the immune response process on the Rodin platform.For the validated model,ProB is used for further model checking for deep optimization,eliminating serious vulnerabilities such as error states and deadlocks that still exist in the model,enabling a safer and smoother transition to the programming and coding stages in the future;In terms of key software systems,this project focuses on elevator systems and mainly studies the application of Event-B in key systems.ProB is used to simulate and validate the system model through animation,and BMotionWeb is used to visualize the model,increasing its comprehensibility and interactivity,and improving the quality of the software.This article is divided into six chapters,and the main research topic is the application of formal method Event-B in complex software systems-immune systems and safety critical software systems-elevator systems.Firstly,the entire process of Event-B method modeling,proving,verifying,and animation simulating the immune system is elaborated in detail.After all proof obligations are released and all verifications are passed,the immune system is implemented using programming language.Secondly,the Event-B method is used to model,validate,and fully visualize the elevator system,greatly reducing errors in the elevator model.The main innovation points of this project include the following aspects:(1)Use ProB to animate and verify the immune model,ensure that there are no deadlocks and invariant violations in the model,ensure the effectiveness of the model,and successfully simulate the artificial immune system.(2)The Event-B method is used to model and demonstrate the safety critical software elevator system.The Rodin platform’s built-in prover and interactive proof are used to release all proof obligations generated by the model,and the ProB verification tool is used to perform animation simulation and model verification on the elevator system.(3)The use of the visualization tool BMotionWeb for visualizing elevator system models greatly improves the readability and comprehensibility of elevator system models.In short,the formal method Event-B,which is more suitable for software requirement modeling in complex software systems,is more applicable.The application of Event-B in security software systems with high security requirements is relatively successful,and it always contributes to the correctness,ambiguity free,and effectiveness of software requirements. |
