17-03-2014, 07:08 PM
Software system validation and verification is the tedious
and arduous process of demonstrating that a software
program correctly implements its requirements specification.
There are two major approaches to performing such
validations: testing and formal proofs of correctness.
Testing involves executing a program with a known set of
inputs and analyzing the results; formal proofs of correctness
involve proving that the expected results are as required for
all valid inputs.
The Boeing Company uses the testing approach to validate
that software it delivers for the Airborne Warning and
Control System (AWACS) aircraft adheres to the complex,
real-time communications protocol required. Over the past
ten years, Boeing has expended millions of dollars validating
the AWACS baseline and subsequent software releases. A
test consists of (1) recording on a magnetic tape periodic
snapshots of computer memory for a pre-determined
scenario from a laboratory simulation of an AWACS
mission, (2) printing a selected portion of the
snapshots,which results in printout that is more than 6
inches thick, and (3) hand analyzing the printout for
compliance. When challenged by a government contract to
prototype a tool that would improve software engineering
productivity in this validation area, we responded by
developing an Automated Software Verification (ASV) tool
that supports encoding the hand-analysis as the rulebase of
an expert system and abstracting the computer memory
snapshots to supply basic knowledge of what occurred
during the laboratory simulation. Encoding the handanalysis
is done by representing specific protocol
requirements and the test engineer's temporal reasoning as
situationlaction rules. Abstracting the snapshots is done
with a two step process that translates (1) from the bits and
bytes on the recording tape to representations of JOVIAL
program data structures in a relational database (2) to
representations of time-ordered significant events as
forward-flowing sequences of facts available to the
knowledgebase. For instance, the program data structures
contain friendlyhostile identification, position, and heading
information about other aircraft derived from local sensors
and messages sent from other monitoring stations about
these same aircraft. A significant event might be an
incoming message whose identification showed an aircraft as
hostile when the local value indicated friendly. The protocol
for resolving such differences is very elaborate.
The salient characteristics of the problem of validating
software for a communications protocol are: (1) the rules of
behavior were contrived by humans as opposed to natural
law; (2) the behavior of interest can (must) be described
unambiguously; (3) the data to be analyzed describe the
states of a system and are time tagged, and (4) there is a high
volume of data. Our successful demonstration of the
prototype tool shows how well the ASV approach fits this
problem.
and arduous process of demonstrating that a software
program correctly implements its requirements specification.
There are two major approaches to performing such
validations: testing and formal proofs of correctness.
Testing involves executing a program with a known set of
inputs and analyzing the results; formal proofs of correctness
involve proving that the expected results are as required for
all valid inputs.
The Boeing Company uses the testing approach to validate
that software it delivers for the Airborne Warning and
Control System (AWACS) aircraft adheres to the complex,
real-time communications protocol required. Over the past
ten years, Boeing has expended millions of dollars validating
the AWACS baseline and subsequent software releases. A
test consists of (1) recording on a magnetic tape periodic
snapshots of computer memory for a pre-determined
scenario from a laboratory simulation of an AWACS
mission, (2) printing a selected portion of the
snapshots,which results in printout that is more than 6
inches thick, and (3) hand analyzing the printout for
compliance. When challenged by a government contract to
prototype a tool that would improve software engineering
productivity in this validation area, we responded by
developing an Automated Software Verification (ASV) tool
that supports encoding the hand-analysis as the rulebase of
an expert system and abstracting the computer memory
snapshots to supply basic knowledge of what occurred
during the laboratory simulation. Encoding the handanalysis
is done by representing specific protocol
requirements and the test engineer's temporal reasoning as
situationlaction rules. Abstracting the snapshots is done
with a two step process that translates (1) from the bits and
bytes on the recording tape to representations of JOVIAL
program data structures in a relational database (2) to
representations of time-ordered significant events as
forward-flowing sequences of facts available to the
knowledgebase. For instance, the program data structures
contain friendlyhostile identification, position, and heading
information about other aircraft derived from local sensors
and messages sent from other monitoring stations about
these same aircraft. A significant event might be an
incoming message whose identification showed an aircraft as
hostile when the local value indicated friendly. The protocol
for resolving such differences is very elaborate.
The salient characteristics of the problem of validating
software for a communications protocol are: (1) the rules of
behavior were contrived by humans as opposed to natural
law; (2) the behavior of interest can (must) be described
unambiguously; (3) the data to be analyzed describe the
states of a system and are time tagged, and (4) there is a high
volume of data. Our successful demonstration of the
prototype tool shows how well the ASV approach fits this
problem.