Second Approach

The second approach is more pragmatic and can be applied to an existing code base. It consists in starting with rebuilding the specifications of the ToA. Indeed, the ToA might work quite well, but you might want to analyze it in detail to find more bugs or to even confirm that no bugs remain. Prerequisites to this work are

• Existing documentation on the target C code: Internal documentation on what the code does and how it's done is desirable, especially when the program contains programming hacks and tricks. Many websites contain valuable documentation on the Linux kernel such as http://www.kernel.org or http://www.tldp.org/. Collections of books, such as this one, might be useful too.

• A specification support tool: Writing a specification is certainly valuable, but error prone. Therefore, it is better to use a specification tool to analyze the consistency of a specification and even to evaluate its pseudo-code.

• The source code of Linux or at least of the ToA.

• Sufficient time and effort.

• A precise definition of the ToA.

Given these elements, you begin to build the specification of the modules that are used by the ToA and considered correct. Their specification consists of a set of modules containing models of variables, constants, and functions. The functions have associated pre- and post-conditions. This assumptions phase necessarily occurs at the basic libraries phase, where basic mathematical functions are models functions. This is predefined in the tool. For instance, the mathematical cosine function models the cos operator on reals.

Then, functions of the ToA are reverse engineered by successive layers: Starting from the lowest layer of functions, its specifications are written and its correctness proven. You can then move on to the next layer assuming that every lower-level is correct.

Depending on tool support, the correctness proof can be more or less automated. Two cases can be distinguished:

• The tool supports the C language natively (such as Caduceus or CAVEAT) The pre- and post-conditions are associated to the functions by inserting them either as comments into the code or as separate files. Verification conditions are generated automatically and their proof is done by an integrated theorem prover.

• The tool does not support the C language (such as B) In this case, the verification conditions and the conformance proof can be done by hand or you must reverse-engineer the ToA code into pseudo-code and perform the same steps as previously done with mechanical assistance. Notice that the translation step is rather risky and the correctness of the reverse-engineered code does not guarantee the correctness of the initial code.

Was this article helpful?

0 0
The Ultimate Computer Repair Guide

The Ultimate Computer Repair Guide

Read how to maintain and repair any desktop and laptop computer. This Ebook has articles with photos and videos that show detailed step by step pc repair and maintenance procedures. There are many links to online videos that explain how you can build, maintain, speed up, clean, and repair your computer yourself. Put the money that you were going to pay the PC Tech in your own pocket.

Get My Free Ebook


Post a comment