The three dimensions of formal validation and verification of reactive system behaviors
Abstract
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.
NPS Report Number
NPS-CS-07-008Related items
Showing items related by title, author, creator and subject.
-
Towards the Dynamic Contracting of Verification Activities With Set-Based Design: An Initial Model of Rework
Xu, Peng; Salado, Alejandro (Monterey, California. Naval Postgraduate School, 2019-04-30); SYM-AM-19-050This paper is intended to disseminate initial outcomes of the NPS Research Acquisition Program “Dynamic Contracting of Verification Activities by Applying Set-Based Design to the Definition of Verification Strategies” ... -
An analysis of Specware and its usefulness in the verification of high assurance systems
DeCloss, Daniel P. (Monterey, California. Naval Postgraduate School, 2006-06);Formal verification is required for systems that require high assurance. Formal verification can require large and complex proofs that can drastically affect the development life cycle. Through the use of a verification ... -
A Mathematical Framework to Apply Tradespace Exploration to the Design of Verification Strategies
Salado, Alejandro; Farkhondehmaal, Farshad (Monterey, California. Naval Postgraduate School, 2018-04-30); SYM-AM-18-105This paper is intended to disseminate some initial outcomes of the NPS Research Acquisition Program's "Tradespace Exploration for Better Verification Strategies"project. The research addresses the design of verification ...