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

Because of the development of Internet technology, people’s lives is entering the information age. Internet which profoundly affects human’s daily needs has become a necessity for people.Various types of software do have brought great convenience to people’s lives, so greater and more extensive demands are being placed on the software. For the growing complexity of software requirements, How to improve the reliability of software and guarantee the quality of software are becoming a hot topic of software engineering which can realize the value of the software to the social.Researchers have been studying how to improve the reliability of software. One of those method is using formal method to describe, reason and verify.B method is a typical formal method which can support the entire process of software development. It has a strict mathematical theory basis and perfect auxiliary support tools to support software development described in the statute, and the statute of stepwise refinement. B method which has a normative and unambiguous, can do reasoning、verification and ensure consistency.However,formal method is difficult to describe the system requirements and it is also difficult to be understood, so in the development it is hard to be used and limited. Many researchers use non formal method to describe the demand, and then use formal method to reason and verify. The Unified Modeling Language(UML) which is semi formal is widely used as a bridge between natural language and description of formal.The method which combines the advantages of UML and formal method B describing high confidence software has been widely used. Although UML can provide a visual interface, is easy to be understood and used, and supports the whole process from requirements analysis to software development, it lacks the description of the behavioral semantics which do that expression of semantic is incomplete and inaccurate.This paper extends the class diagram,state diagram and sequence diagram of UML-based online examination software system by using UML extensibility mechanism and map it to the B formal method.It will deduce and prove the needs, and ensure the high reliability of software.