Formal Vs Semiformal Methods

You can't rely on people being careful and using programs in a controlled manner. Some programs are extremely complex and made up of numerous modules that interact. Operating systems are a good example. Applying current knowledge, the steps to producing very reliable software are as follows:

1. Control the tools used. A prerequisite is to use well-established tools (such as the gcc compiler chain) and avoid dubious tools, where the results are uncertain. Tools evolve during the development process, and therefore new versions must be tested against the old features used (some gcc 2.96 compilers had flaws, for instance). At a higher level, languages that are easy to write and analyze are preferred. For instance, Ada with its rigorous semantics is a good choice. Ada is also a good choice because it serves as the backend to the B formal method1 that, using a series of refinements, produces Ada code that can then be compiled normally into binary code, using the GNAT compiler for instance.

2. Control the process used. Many process types exist, ranging from V-shaped lifecycles to iterative prototyping cyclic lifecycles. Processes can be controlled in terms of product output (specification, design, detailed design, testing documents, etc.) and checked for conformance with respect to procedural standards (ISO 9000 or Common Criteria for IT Security, for instance). Processes contain control points where you can examine the results (review code, check tests against specifications, etc.), and you can make sure these products are delivered effectively.

3. Use formal techniques for every possible task during the process. Develop formal specifications and designs, and prove the code produced by the implementation is correct. This is the essential part, making use of mathematical objects (sets, mappings, relations, etc.) to build mathematical models of objects involved in the problem at hand; models can then be used (similar to algebraic formulas) and properties of these models (such as correctness) can be proven. Formal techniques can be partially applied, meaning that only selected parts of the problems are handled, in which case a formal specification without proof (see "Analyzing C Code Using Hoare Logics") is sufficient.

4. Test the code systematically. Testing is complementary to the previous steps as it helps you understand the code's behavior, test incomplete code in some specific cases (for instance, at domain boundaries), and correct it until it performs satisfactorily. Then, you can apply a formal analysis to treat the general case.

5. Measure the code's complexity. In particular, measure its processor and memory consumption to verify if it's adequate for the target platform characteristics and constraints. Indeed, some design choices might be elegant but inefficient.

1. See J. R. Abrial's The B Book: Assigning Programs to Meanings, Cambridge University Press, 2005.

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