29-05-2010, 12:23 AM
One of the key step in formal verification is the construction of a formal model of the system to be verified and these models can be visualized as a finite state machine. And model checking is the technique of systematically verifying a system against a set of intended properties. Any Model Checker thus explores all possible interleaved executions of the state machine. Given a specification of the system in terms of a finite state machine and property to be verified, model
checker automatically explores the state space in order to find an execution sequence that causes the violation and thereby helping in finding the bug.
One of the main problem with model checking is the state space exploration, for, state space grows exponentially with the number of processes and thus making it infeasible to be solved even in modern machines. Again, model checkers
have their own specification language to model the system and it is not at all trivial to extract the model from the code written in high level programming language. Again, solutions to these problems should supplement each other. Abstraction is one of the central method of addressing both these problems in conjunction, where one tries to get rid off unnecessary details of a code irrelevant to a property. Tools for automated abstraction assist in the automated extraction of verification models from code as otherwise model becomes too detailed to be
useful. SPIN being a model checker accepts a specification language called PROMELA. FeaVer is
one such tool of automatically extracting PROMELA model directly from a C-code, but involves a huge amount of manual intervention. abC is a tool from Bell Labs that automates the process of hiding data in C code. One common problem
with both these tools are, they don't descend into the procedure call hierarchy, and hence can only work at procedure level. Both the tools have indicated that data hiding and data narrowing are promising candidates for abstraction, but none of the tools have tried to unify these two promising candidates of abstraction. In fact, no work on data narrowing has been found present in the literature.
We thus aim to solve the following problem - i) To automatically find out the set of variables from a C-code which can be omitted from the model taking into account the procedure call hierarchy. This is an extension of the work being
done previously. ii) To automatically identify a set of variables whose type can be narrowed down