Towards Automatic Model Extraction

One of the crucial steps in formal verification is the construction of formal model of the system being verified. Usually formal models are constructed from informal design documents. But such documents are often ambiguous and do not reflect the actual system: many decisions taken at the time of implementations are not documented. In such cases, the applicability of verification results is questionable.

The objective of the project is to build verification models directly from the code automatically to avoid the above problems.

A prototype tool that extracts finite state models of C programs is developed. Besides the input program, a set of variables of interest is input to the tool. Techniques of slicing and abstract interpretation form the basis of the tool. The slicing tool UNRAVEL and data flow analysis tool LDRA are used for extraction. The extracted finite state model can directly be input to the tool STeP for verification.

A prototype version of the tool is ready. Currently, the tool accepts a very restricted subset of C: it includes only basic data types like integers and strings and all simple control structures like conditional and iterative constructs. Structures and pointers are not included in the subset. The tool needs improvement. A larger subset of C has to be considered, the ultimate goal being the entire MISRA-C subset; an extensive library of abstractions is to be built to carry out a variety of abstractions that are required in practice.