The three dimensions of formal validation and verification of reactive system behaviors
Loading...
Authors
Drusinsky, D.
Michael, J.B.
Shing, M.
Subjects
Computer programming
Software
Software engineering
Automation
Software
Software engineering
Automation
Advisors
Date of Issue
2007-08
Date
Publisher
Monterey, California. Naval Postgraduate School
Language
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.
Type
Technical Report
Description
Series/Report No
Department
Computer Science (CS)
Identifiers
NPS Report Number
NPS-CS-07-008
Sponsors
NASA IV&V Facility (U.S.)
Funder
NASA IV&V Facility (U.S.)
NNG07LD01I
NNG07LD01I
Format
ii
Citation
Distribution Statement
Approved for public release; distribution is unlimited.