Automatic test cases generation from formal contracts

Context: Software verification for critical systems is facing an unprecedented cost increase due to the large amount of software packed in multicore platforms generally. A substantial amount of the verification efforts are dedicated to testing. Spark/Ada is a language often employed in safety-critical systems due to its high reliability. Formal contracts are often inserted in Spark’s program specification to be used by a static theorem prover that checks whether the specification conforms with the implementation. However, this static analysis has its limitations as certain bugs can only be spotted through software testing. Objective: The main goal of our work is to use these formal contracts in Spark as input for a test oracle - whose method we describe - to generate test cases. Subsequent objectives consist of a) arguing about the traceability to comply with safety-critical software standards such as DO-178C for civil avionics and b) embracing the best-established software testing methods for these systems. Method: Our test generation method reads Spark formal contracts and applies Equivalence Class Partitioning with Boundary Analysis as a software testing method generating traceable test cases. Results: The evaluation, which uses an array of open-source examples of Spark contracts, shows a high level of passed test cases and statement coverage. The results are also compared against a random test generator. Conclusion: The proposed method is very effective at achieving a high number of passed test cases and coverage. We make the case that the effort to create formal specifications for Spark can be used both for proof and (automatic) testing. Lastly, we noticed that some formal contracts are more suitable than others for our test generation.