9 Ekim 2007 Salı

Software Verification

A program is a mathematical object. A programming language is a mathematical language. Therefore, proving properties of a program should be possible. Does the program do what is supposed to do? Does it not do anything harmful? Is it possible to answer these questions?
In spite of the fact of being a mathematical object for a program, the answer is probably no if we think about all. A programming language is also a formal language. By the definition, the set of inputs upon which a certain Turing Machine halts. This definition denotes that each well formed program would compile or not. The compiler itself is a program too. According to this induction, perhaps it seems possible to prove properties of every program. But it is not.

Turing machine halting problem is NP-complete. In complexity theory, the NP-complete problems are the most difficult problems in NP (nondeterministic in polynomial time). It is not possible to decide when the program terminates this is why the Turing machine halting problem is NP-complete. It is possible to prove sequential programs. You do only some checks on the actions the program do. But loops used inside a program makes deciding very hard. Proving loops properties requires constructing a loop invariant. The loop invariant is often the inductive property one has to prove of a recursive program that is equivalent to a given loop.

According to Rice Theorem, every interesting question about the behavior of programs is undecidable (1953). Software verification problem is undecidable; so it is not possible to talk about NP-completeness which is valid for only decidable ones. Although problems related with the behaviors of programs are undecidable, they are classified as recognizable. This means, we can get answered if the answer is true. The problem is asking the right question.

Software verification is the act of proving or disproving the correctness of an abstract model that will be realized against its formal specifications. It provides the answer to the question: “Are we building the product right?” There are two methods of verification: Theorem proving and model checking.

Theorem proving is a technique where both the system and its desired properties expressed as mathematical logic formulas. The logic is given by a formal system, which defines a set of axioms and a set of inference rules. Then, theorem proving is the process of finding the proof of property from the axioms of the system by applying inference rules. Steps in the proof appeal to the axioms and rules, and possibly derived definitions and intermediate lemmas. Although the proof could be constructed by hand, since systems becoming large and complex, it is not reasonable. Hence, there has been a great effort on developing theorem provers with various degree of automation, and also proof checkers have been proposed to confirm the correctness of the proof. Another way is the interactive theorem prover. By definition, it requires human assistance which causes the process to be slow, and error-prone. Prolog is the commonly used tool for theorem proving.

Model checking is a widely used verification technique that is model-based, automated, using a property verification approach, mainly useful for verifying concurrent and reactive systems, typically in a post development stage. The overall behavior of a distributed system is modeled as a transition system, whose states represent the global states of the distributed system, and whose transition relation gives the possible evolutions of the system. It can be checked whether such a transition system is a model of a temporal logic formula. There are several tools used in industry. SPIN performs software verification at design time over its programming language called Promela. Also JavaPathFinder verifies java code. You add a special class (Verify) inside your java code.

In contrast to the theorem proving model checking is completely automatic and fast. Model checking is used to check partial specifications; therefore it can provide useful information about a system’s behavior without checking the whole system. Above all, model checking outputs counterexample if the given property doesn’t hold by the model, which usually represents the subtle errors in design, and thus can be used to help in debugging.

It might be possible to find some software bugs by using verification either using theorem proving or model checking. But it is not possible to find all. Same thing is valid for defects. Also Dijkstra supported my idea in 1972: “Program testing can be used to show presence of the bugs, but never to show their absence”

In conclusion, this problem is undecidable but recognizable. It is possible to verify a software product under some conditions. This does not conflicts with undecidability, as undecidability is defined each element inside domain. This problem is undecidable and the answer of the question is not yes for each software product.