Promela Model Extraction - PROMET
About
PROMET -- Promela Model Extractor -- is a compiler from arbitrary complex C code to PROMELA using tabled abstraction. That way created models can then be verified for specific properties with the SPIN Model Checker. The properties are specified using a language similar to Microsoft SLAM's SLIC specification language called SPEC.
Specification Language
SPEC adapted SLIC's pre- and post conditions on function interfaces to express a property of interest. Suppose you want to verify that no call to kmalloc contains a negative argument then this could be expressed in SPEC like this:
void SPEC_kmalloc_call(int size) {
if(size <= 0)
assert(0);
}
The original source will get instrumented with a function call to SPEC_kmalloc_call in front of every kmalloc call. Whenever a path in the original source code leads to a kmalloc call with a negative argument then this SPEC specification will abort.
Model Extraction
The instrumented C source code is then translated to PROMELA, together with the specification functions. This process is called model extraction. The following translation rules apply:
- Every local variable becomes a global variable ensuring a unique naming scheme, the same applies for return values.
- Every C function becomes a C preprocessor macro.
- Every constrol structure is rewritten to promela control structures.
- Every C statement is rewritten to Promelas c_code { } construct, c_expr {} for expression.
Environment initialisation
The environment of a given source code module is any datastructure or function which is not part of the code but which is referenced in the code. Since the analysis is statically done this environment is not available and must be provided artificially. PROMET is using a lazy initialisation algorithm introduced by Khurshid et. al. [1] which tries to initialize the environment with the needed values. A simple example: given that the variable a is from the environment and the following code snippet is in the inspected source code:
if(a > 10) {
// do something
}
There are obviously two paths over this piece of code. One where a is bigger than 10 and one where it is smaller than 10. Since we are interested to inspect every path the model contains the lazy initialisation algorithm will non-deterministically assign a a value bigger and smaller than 10 (in this case probably 9 and 11).
This is just one example of initialisation. Other constructs which have to be initialized are: pointers, function pointers, formals of leaf functions in the call graph, etc.
Download
You can download the source code here: promet-0.1. All rights are as stated in the tarball.
Bibliography
[1] Sarfraz Khurshid, Corina S. Pasareanu, and Willem Visser. Generalized symbolic
execution for model checking and testing. In TACAS, pages 553568, 2003.