A Study Of Software Formal Requirements Based On Event-B

The Requirements Engineering appears in the mid 80's of last century and has already become an independent research branch of the software engineering currently.The study on the technique of capturing software requiements is very important in requirements engineering. How to cook the rigorous and elaborate software requirements in an appropriate method affects not only the understanding and communicaiton of software system, but also the success or failure of final software products, especially in the development of the safety and critical System.There are two kinds of main ways to elicit software requirements at present: Natural Language and Semi-formal Method.Natural Language is the preferred tool to capture software requirements in the development of software product now. The most important tool of semi-formal method is UML/OCL. There exist inconsistency and semantic ambiguity in natural language, the modeling elements of UML lack of rigorous formal semantics, they can not produce precise requirement model of software system. Although the ambiguity of system blue-print can be reduced in the certain degree by introducing OCL in UML, but triple-value logic of OCL still can't eliminate the ambiguity of UML model fundamentally.Software requirements and their construction process based on these two kinds of ways have a lot of bugs and defects.The errors in requirements can be probed by the test, but the test can not find the flaw in requirements. The formal methods which based on strict mathematic semantics can specify and verify a software system and its property clearly, accurately, abstractly, and concisely. It can find the defects in requirement model, and improve safety and reliability of software greatly. However, there are no cases of successful application of formal method in the requirements construction process.According to this, the thesis put forward a requirements analysis way based on formal methods.First, on the basis of basic discrete system, a system model--Fair Discrete System Model which can be applied in any phase of software development process-- is proposed.The refinement, verification, method of controlling complexity and reusage of system model in requirements elicitation process are accurately and concisely discussed. Next, the whole process of formal requirement is completely discussed in formal specification language Event-B, the model structure of Event-B is extended in the paper, and the conception of refinement and verification from specification to program are extended to the requirement phase. The concept's difference of refinement and verification in two phases are explained in detail. In the method of controlling complexity of model, a new model decompose arithmetic is present,a new strategy of introducing new event in the refinement is put forward, and a new tactic of reusing requirement model is given. Correspondingly, taking the subsystem of Scenery Management System- the Guard System- as example, this paper elaborates the application of this method in practice. Because the Event-B only consider liveness and its proof obligation under mini-progress fairness, this paper give a direction of future work in last part.