ClawZ: Cost-effective formal verification for control systems

Abstract

Control system software now plays a key role on many platforms, including aircraft and automobiles. However, as control system software has been performing increasingly complex tasks, the associated software development, maintenance and certification costs have escalated significantly. The ClawZ toolset is dedicated to the formal verification of control system software. By using some novel ideas, it achieves the highest levels of assurance whilst not suffering from the prohibitively high costs normally associated with applying formal verification. It has been successfully used in the certification of the Flight Control Computer of the Eurofighter Typhoon aircraft. This paper outlines the toolset, and explains how the approach used to build it enables formal verification costs to be dramatically reduced whilst not compromising on soundness. © Springer-Verlag Berlin Heidelberg 2005.