Invensys Triconex uses the abstract interpretation method in its Trident TMR controller system, which provides continuous control for safety-critical units in refineries, petrochemical and chemical plants, and in other industrial processes. The firm says abstract interpretation has saved $1 million and up to a year in verifying fault-tolerant controller software used in process manufacturing applications that need high levels of reliability and availability.

Trident provides fault tolerance via a triple-modular-redundant (TMR) architecture, which integrates three isolated, parallel control systems and extensive diagnostics. Required before each new product release, testing is a challenging task for a system that may have, for example, approximately 70,000 lines of C code, 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.

Triconex says the challenge here is detecting runtime errors, such as processor halt, data corruption, timing violations, etc. A complete "white box" test of such a product can easily take four or five person-years of effort, spread over six to 12 months to satisfy Invensys' quality requirements and obtain certification from government agencies.

The abstract interpretation method uses an abstraction of the analyzed software built from its dynamic properties. Triconex used Verifier from PolySpace Technologies. This is an abstract interpretation tool that evaluates code one time from its dynamic properties, which reduces the computational load. The advantage of this approach to software verification is that it can automatically check 100% of runtime errors in a fraction of the time otherwise required to test code using traditional verification methods. www.triconex.com and www.polyspace.com

• Triple-modular redundant controller applied to safety, critical process control applications
• Designed to withstand harsh industrial environments
• Allows online maintenance without disturbing the process
• Optimized for critical applications with small to medium point counts