Testing Functional Requirements using B Model Specifications

Abstract

Testing is very important part of software development. Almost 80% software fails because of the improper or inefficient testing. Testing is performed by different types of strategies. Generally testing is performed on code, but if the software can be tested in the earlier phases then most of the errors can be eliminated and can be stopped from propagating to next phase. Thus there is a need to explore testing possibilities in earlier phases. The proposed work presents a novel requirement based testing approach that can fix errors in initial phase. Formal Specification languages play a vital role in software testing. Formal models provide a precise specification of the system, and can be used as a vehicle for driving the development process. To perform requirement based testing, we need a formal language that can deal with the requirement specification efficiently. Many researchers have proposed various approaches to generate test cases from formal specifications. These approaches include test case generation from various state based languages like Z, VDM and B specifications. We investigate, why B specification is more appropriate than Z and VDM for test case generation in proposed work. We also compare test case generation from above specification languages and find limitations of each approach. In this thesis work we proposed a technique that can provide better coverage of requirements as compared to other approaches. For maximizing the coverage of requirements in our model, we annotate our specifications with requirement identifiers, which help in later stages to detect which requirements are covered and which are yet to be tested. Test cases are generated by extracting invariants and postconditions from our specification, and are transformed in a generalized form. Using test selection criteria, we can cover all parts of our model and generates test cases for each of our test objective.