Software Tool enhances safety control of critical software.
Share:
Press Release Summary:
Based on proof techniques and static analysis of software, Caveat helps users verify software and systems in development. It detects errors when result does not have expected properties, and highlights possibile errors in execution of software. Tool indicates reasons for failure, details various cases where errors could occur, and demonstrates that error will not occur given proper conditions of software operation.
Original Press Release:
Caveat, a New Tool to Ensure Reliability of Critical Software for Control System Applications
Chicago, January 20, 2004
Omnipresent throughout our everyday lives, software sometimes contains bugs. Some of this software is used in aircraft control systems, for example, where security and reliability are extremely important. Researchers at the French Atomic Energy Commission (CEA) recently developed an innovative software tool called Caveat that enhances safety control of critical software.
Caveat is the result of more than ten years of research at the Laboratory for Technology and Systems Integration at the CEA. The development of this tool was funded by the CEA, Airbus France, and EDF, the French electrical utility company. The latter partners tested the tool throughout its development, ensuring that it meets the needs of industry. Airbus France is using Caveat to verify software and systems in the course of development and, in its first specific application, to test a subset of critical safety software for flight controls on the A380 program. EDF is using it to verify the reliability of critical software developed by subcontractors and supplied in turnkey systems.
Software is said to be critical when an error in its execution can have an impact on people's safety or serious repercussions for the system that it controls. This is the case, for example, for the command and control systems in a nuclear power plant, flight controls for an aircraft, or the control system for a driverless train.
Critical systems in IT as well as in other fields (mechanical engineering, electrical engineering, etc.) have to be safe. This necessity is all the more important in view of the increasing computerization of everyday systems. For example, the average automobile today contains as much software as an Apollo rocket of the 1960s and 1970s. To ensure the safety of critical software, designers follow a rigorous approach in their choice of developers (highly qualified and experienced personnel), development methods (choice of development language, operating system, etc), and verification strategy.
Testing is the most widely used technique for verification. It consists of performing multiple executions (known as dynamic analysis of the software) with input data estimated to be representative of the conditions of use. The number of tests that would need to be performed to be certain of the verification of the software is too large to be practicable, even with the most powerful computers. It is therefore necessary to limit the cases tested to those estimated to be representative of real uses of the system.
The verification stage of software development represents on average half the cost of developing critical systems. In aeronautics it can be as high as 80% of the cost. It is, therefore, a key factor in the commercialization process in terms of cost control and time to market. These constraints are further increased by pressures of competitiveness.
In addition, correcting an error in software is vastly more expensive if it is detected late. Early detection of errors can be carried out before the testing stage with the use of static analysis tools, that is, tools that do not execute the software. The result of this analysis is valid for all software operations, whatever the input values, and not just for certain sets of values as is the case for testing. It is with precisely this approach that the Laboratory for Technology and Systems Integration (LIST) at the CEA has developed Caveat, an innovative software tool that enhances safety control in critical software in industry.
Caveat is based on proof techniques and static analysis of software. The tool mainly detects errors when a result does not have the expected properties. It also highlights possibilities of errors in execution of the software such as infinite loops and division by zero. Its principle of operation consists of comparing the software to be verified, which can consist of some tens of thousands of lines of code for example, with the property expected from the result, which is expressed by a mathematical formula only a few lines in length. From this comparison, Caveat formulates a mathematical condition: for example, for the result to be as expected, the parameter "a" must be less than zero.
The user then verifies that this parameter is less than zero in all cases. If so, this is taken as proof that the result corresponds to an expected property. If the proof fails, the tool gives indications as to the reasons for the failure. In most cases, this will be due to insufficient assumptions, which then need to be clarified.
While other static analysis software tools on the market simply detect possible errors, due to division by zero for example, Caveat is able to detail the various cases where this error could occur. It therefore provides more precise analysis of the causes of potential errors and can also demonstrate that the error will not occur given the conditions of software operation. This refinement of the result is provided through several interactions with the user, whereas other software tools are entirely automatic.
Commercialization and marketing of Caveat will be carried out by the French company TNI-Valiosys.
For more information, please contact:
FRENCH TECHNOLOGY PRESS OFFICE
205 North Michigan Avenue, Suite 3740
Chicago, IL 60601
Tel: (312) 327-5260
Fax: (312) 327-5261
E-mail: contact.ftpo@ubifrance.com
