Early Validation of Functional Requirements and Transition to Source Code with Event-B

Abstract

The cost of fixing software requirements errors after deployment is so high that it is vital to come up with ways to find and fix requirements errors early in the life-cycle of a project. The work in this paper advocates for the use of formal methods as an alternative approach to guarantee the correctness of the software from requirements to code. We present a formal-methods based approach for the early validation of functional requirements. Our approach relies on formal methods techniques such as program refinement, correctness-by-construction (CbyC), and automated code generation. We present two case studies that showcase our approach; for the case studies, we discuss design decisions, flaws encountered, and lessons learned.