The Research Of Formal Modeling Technology Of Software Requirements Based On The Event-B

In traditional software development process, usually taking non-formal orsemi-formal methods as a means of describing software requirements, but thenon-formal methods and semi-formal methods can’t avoid the defects and errors causedby the natural language as the method of describing software requirements, thetraditional software development methods can’t ensure the correctness of softwarerequirements in the requirements analysis phase. The traditional software requirementsmodeling, just like UML modeling describe the functions of the software system in therequirements analysis phase, without providing the ability of verifying the softwarerequirements describetion. The formal method is based on the rigorous mathematicaltheory, applying mathematic means to design, simulate, analysis software systems to geta software system model as precise as mathematical formulas, then using modevalidation as the means to check the validation of the software system model. Thevalidated software system model is accurate, unambiguous, avoiding the flaws anderrors introduced in software requirements and reaching the purpose of insuring thequality of software system.In order to avoid the ambiguity and inconsistency bringed by non-formal methodand semi-formal method, this thesis uses Event-B as a formal specification language tobuild the software system model, firstly based on the Rodin platform stating the stepsand methods of using formal language to found the software model, then stating thewhole process to establish software model and verify the validation of the model. Themain content includes the following aspects:1.The evils of software development bringed by the traditional softwareengineering approach, and the characteristics of formal software requirementsdescription method and the research status of formal method.2.Studying the structure and refinement techniques of the Event-B model, firstlyintroducing the two main components of the context and the machine of the the Event-Bmodel, as well as the relationsheep between them, and then telling the refinement skills, including events refinement skills and state refinement skills, ending with a briefintroduction the function of the Rodin platform.3.Taking tree file system for example to indtroduce the steps and methods to buildthe Event-B model, firstly creating an abstract model of a tree file system, and thengradually adding tree attributes or functions of the file system to the model withrefinement skills inorder to expand and enrich the model. By stepwise refinement,adding some attributes to the abstract model, for example the files and directories of treefile system, the content of the file, processing of power-down accident, the attributes ofthe file system, access control attributes and functions.4.Studying the Event-B model validation based on the Rodin platform, stating theproof obligations, the proof of the inference rules and proof strategies closely related tothe model validation, and the validation process of the tree file system model, helpingthe developers working with formalization software development method to understandthe model validation and the Rodin platform better.5.The conclusion section summarizes the research results and the outlook for thefuture work.This thesis based on the Event-B formal method, taking the tree file systemsoftware requirements as an example to show in details how to describe the softwareattributes and functionality of tree file system, verify the tree file system model basedon the Rodin platform, state the whole process to establish the Event-B formal methodsand verify the model.