Formal verification and legacy redesign

Sustaining weapons system hardware and software represents a significant an d ever-increasing portion of total system cost. Hardware components are bec oming obsolete much sooner while weapons system lifetimes are increasing. W e must identify more cost-effective solutions to engineering and reengineer ing these subsystems. Verifying and validating weapons systems are two of t he most costly parts of either engineering process, Traditionally, hardware validation and verification is done by simulation and testing, In the past few years, math- and logic-based formal methods tools have begun to scale up to and be applied successfully to real-world problems. Incorporating for mal verification methods into engineering and reengineering processes will cost-effectively and significantly improve the level of trust and the quali ty of our weapons systems. Formal methods are especially well suited for re designing current weapon systems which have become unsupportable due to com ponent obsolescence because they help minimize the astronomical costs of ri gorously reverifying the reengineered components. We believe that formal me thods are an important tool for effective engineering of future weapon syst ems.