A High-level Perspective on Formal Validation and Verification
Intervenant(s) : Pr. Shing, (Naval Postgraduate School, Monterey, CA, USA)
In spite of three decades of software formal verification and validation (FV&V) research, there exists no ideal FV&V technique that works well for all FV&V concerns. That is, there is no one technique that enables (i) easy and correct construction of requirement specification of complex real-life properties, and (ii) complete verification coverage of complete real-life complex software with respect to those requirements. Moreover, many of the FV&V techniques are ineffective in handling temporal behavior of reactive systems. In this talk, we present a visual tradeoff space we developed for the US NASA IV&V Facility, called the FV&V tradeoff cuboid, for software engineers to discuss the various tradeoffs (e.g. cost, coverage, etc.) between different FV&V approaches in order to select the appropriate techniques for V&V.