Requirements-based Code Model Checking

Building the system right is the objective of quality assurance methods. Though testing is the most prominent and widely-adopted means, it cannot prove the absence of software's defects. Therefore, static measures such as formal proofs can complement dynamic methods. However, these techniques require the formal statement of requirements, which is still a challenge in industry development. This paper suggests a way of formalizing requirements in controlled natural language in a way that applies directly to C program code. By mapping natural language terms to conditional breakpoints, requirements can be translated to formal language expressed in observer automata. The creation of a mapping between natural language terms and code is supported by natural language processing methods. Finally, the observer automata are model checked against the code. In our approach we demonstrate the described steps using a set of realistically shaped requirements, which are common in the avionics domain. We implemented a simple tool hiding the abstract and mathematical details, which performs the proofs automatically. The paper is presented as an approach towards the seamless verification of code against requirements typically found in the avionics domain.