The three dimensions of formal validation and verification of reactive system behaviors

摘要

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 paper we use a cuboid to characterize the trade space among three categories of FV&V techniques. We illustrate the use of the cuboid in tradeoff analysis to determine the appropriate techniques for V&V based on cost and coverage.