Posted: 12th December 2017

Embedded software in the transportation sector (railway, automotive and avionics) needs to meet high reliability requirements because errors may have severe consequences. Research since 2008 by Daniel Kroening’s group at Oxford has developed effective reasoning technology to provide assurance that key error types are eliminated from embedded software, and has created novel algorithms to prove its integrity. Major players from the car industry as well as, GM and Airbus have used technology developed at Oxford to verify the absence of errors. A particular advantage of this technology is its ability to reason accurately about floating-point arithmetic meaning that a much wider class of properties can be verified. The technology is widely distributed via third party operating systems and tool-sets.

Since late 2009 the new technology in Validation and Verification (V&V) and safety certification has been adopted by a number of major systems vendors, especially in the automotive sector, as follows:

• Tata Consultancy Services (TCS), based in India, is the largest IT employer in the world and primarily targets the automotive market. TCS has integrated CBMC into its AutoGen test generation tool, and states that

To the best of our knowledge CBMC is the only tool that supports floating point operations that match the precision of the target platform and yet scales to industry size code. Tata Consultancy Services (TCS)

• They also confirm that CBMC has enabled them to identify bugs and unreachable code that would otherwise have been missed, and save 'a large amount of time'. Additionally TCS has used CBMC to improve the precision of static analysis, reducing around 68% (and in one case 100%) of false positives generated, and leading to 'a substantial saving in manual efforts overall'.

• General Motors in India has used the reasoning technology available via CBMC to validate C programs generated from Simulink diagrams. CBMC has been integrated into GM’s in-house verification tool.

• A major automotive company have given presentations at Oxford University demonstrating the benefits to them of CBMC.

• More recently (May 2013) a German automotive supplier, BTC-ES, has used the reasoning technology to make significant improvements to the V&V tool which they market; a BTC-ES research engineer reports that 'specific floating-point issues were not taken into account within the BTC-ES internal tool chain and in the internal formats, among them floating-point casts, rounding modes, exact string representation of floating-point numbers. The latter circumstance establishes a clear and evident argument for the inconsistent tool behaviour since the semantics of the original C program was not accurately reflected within the data structures and algorithms of the BTC-ES tools. With the expertise of the Oxford team all these issues could be resolved such that sound analysis results are now obtained.'

• In the aeronautics sector the technology has been applied by Airbus where, during the CESAR project, the CBMC tool was used in the X-man Verifier to verify models in the avionics industry. The project team including staff from Oxford and from Airbus conducted a case study on a representative avionics application – the Ground Fuel Transfer function of a large transport aircraft. It models the specific behaviours of the fuel management system when the aircraft is physically on the ground, as opposed to behaviours while the aircraft is in flight.

Other areas of industry have also used tools such as CBMC which have the new reasoning technology embedded within them to perform V&V and safety checking. For example:

• South Korea's Advanced Power Reactor's Reactor Protection System is concerned with safety-critical systems in nuclear reactors. Research published in 2011 showed that 'the HW-CBMC reduces cost by providing automated way of establishing the consistency of HDL implementation using the ANSI-C implementation as a reference, because debugging and testing cost of the ANSI-C implementation is usually lower.'

• The Air France crash of 2009, in which a plane crashed into the Atlantic killing everyone on board, was caused by an airspeed measurement malfunction. Researchers at Galois (a US high assurance R&D software company) and the US National Institute of Aerospace have demonstrated that, in relation to airspeed measurement systems, 'CBMC can prove that the C code is memory-safe, including proving there are no arithmetic underflows or overflows, no division by zero, no not-a-number floating point values, no null-pointer dereferences, and no uninitialized local variables.' CBMC has thus provided further reassurance about the safety of such airspeed measurement systems.

To give an indication of how widely available CBMC is, it is contained in the standard distribution of the Ubuntu, Fedora and Debian versions of Linux. Debian alone has over 10m installations.