A Viable Approach to Formal Verification of Complex Aerospace Systems
Design Verification is playing a growing role in building physical systems largely controlled by software. This is driven by the often acute and sometimes chronic rise of project cost and duration brought on by the increase in testing now needed. Formal methods, as a subset of Design Verification, offer the promise of exposing design and requirements anomalies very early in the engineering process. In practice, achieving these benefits has been hampered on the one hand by the need for highly specialized skills, and on the other by a lack of significant computational power needed for the largest, most complex systems, where the potential value is the greatest. But there are signs of an inflection point, and rigorous design verification is already being applied in a number of industries and companies. This inflection point is a product of three forces: 1) The increase of affordable and usable computational power, 2) the invention and optimization of new efficient algorithms, and 3) the availability of robust tooling that exploits both power and efficiency.