A relatively new method, abstract interpretation, is a process for automatically checking dynamic properties of software applications without actually running any test case and without executing it. Triconex—a unit of Invensys that supplies products, systems, and services for safety, critical control, and turbomachinery applications—uses abstract interpretation in its Trident system...
|
A relatively new method, abstract interpretation, is a process for automatically checking dynamic properties of software applications without actually running any test case and without executing it. Triconex—a unit of Invensys that supplies products, systems, and services for safety, critical control, and turbomachinery applications—uses abstract interpretation in its Trident systems, which provide continuous control for safety-critical units in refineries, petrochemical and chemical plants, and other industrial processes. According to the company, the abstract interpretation method has saved $1 million and up to one calendar year in verifying fault-tolerant controller software used in process manufacturing applications that require a high degree of reliability and availability.
Trident controller provides fault tolerance by means of a triple modular redundant architecture that integrates three isolated, parallel control systems and extensive diagnostics. Testing, required before each new product release, is a very challenging task for a system that has approximately 70,000 lines of C code and 140,000 lines of Ada code, and operates in triplicate in hard real time so it can shut down a plant within milliseconds if specified safety boundaries are exceeded. The challenge was detecting runtime errors, such as processor halt, data corruption, timing violations, etc. A complete “white box” test of such a product can easily consume 4 to 5 person-years of effort, spread over 6 to 12 calendar months to satisfy Invensys quality requirements and obtain certification from government agencies.
The abstract interpretation method works on an abstraction of the analyzed software built from its dynamic properties. Triconex used PolySpace Verifier, from Polyspace Technologies, an abstract interpretation tool that evaluates the code just one time from its dynamic properties, greatly reducing the computational load. The obvious advantage of the new approach to software verification is that it can automatically check 100% of runtime errors in a fraction of the time that would be required to test the code using traditional verification methods.
Gershon Shamay, software development manager for Invensys, says, “The most important improvement [offered by abstract interpretation] is that we are now certain we have examined every line of code under every possible input condition. The certification agencies agree with this assessment. They have encouraged us in the past to move to full visibility verification methods and certified our newest product in record time based on abstract interpretation.”
Polyspace Technologies www.polyspace.com
Triconex www.triconex.com
3 tips for applying abstract interpretation
Apply abstract interpretation to software to:
Protect against runtime errors.
Reduce artificial intelligence execution time, with related adjustment and tuning.
Identify and diagnose problems, including the location of the line of code where the error originated.
