Research On Formal Method For The Online Exam Software Requirement Specification Based On B Method

As the development of network technology, online examination software is becoming a hot topic. Due to the fact that current online examination software developers often use traditional non-formal or semi-formal development method as the described means of the software requirements. However the online exam is a kind of process software which is based on real-time business. Conventional non-formal or semi-formal methods of expression based on the state transition is not complete, lacks accurate semantic information and effective reasoning mechanism, therefore it is not enough to make sure that an online examination software keeps consistent and complete in the requirement analysis.UML model includs the use case diagram and use case specification, so it is easy to understand. But the lack of acurate semantic information will cause ambiguity; At the same time,UML dose not have good reasoning and model checking mechanisms.This dissertation chooses B-Method as formal method, on the one hand the formal B method is based on rigorous mathematical theory; On the other hand it runs through the whole process of programming. Choosing B methods described in the statute, to avoid ambiguity and ensure consistency, helps developers understand the system, reducing the pressure of post-maintenance.The main object of this dissertation include online exam software, use case model and B method. By analyzing the relationship between the constituent elements of the use case model and B methods. Build the mapping between use case model and B method and apply it on the online exam software. Achieve a formal requirements specification description and solve the big problems of online examination system.At last, analysis the online examination process and establish a case mode. Describe the use case modle by mapping rules,test and verify its correctness by tools.