Inference of Properties from Requirements and Automation of Their Formal Verification

Abstract

Over the past decades, various techniques for the application of formal program analysis of software for embedded systems have been proposed. However, the application of formal methods for software verification is still limited in practise. It is acknowledged that the task of formally stating requirements by specifying the formal properties is a major hindrance. The verification step itself has its shortcoming in its scalability and its limitation to predefined proof tactics in case of automated theorem proving (ATP). These constraints are reduced today by the interaction of the user with the theorem prover (TP) during the execution of the proof. However, this is difficult for non-experts. The objectives of the presented PhD project are the automated inference of declarative property specifications from example data specified by the engineer for a function under development and their automated verification on abstract model level and on code level. We propose the meta-model for Scenario Modeling Language (SML) that allows to specify example data. For the automated property generation we are motivated by Inductive Logic Programming (ILP) techniques for first-order logic in pure mathematics. We propose modifications to its algorithm that allow to process the information that is incorporated in the meta-model of SML. However, this technique is expected to produce too many uninteresting properties. To turn this weakness into strength, our approach proposes to tailor the algorithm towards selection of the right properties that facilitate the automation of the proof. Automated property generation and less user interaction with the prover will leverage formal verification as it will relieve the engineer in the specification as well as in proofing tasks.