Introduction to Traditional V&V
• For mission-critical applications such as C2
(command and control) and embedded systems,
the V&V effort can be expensive and labor
intensive. The V&V effort can be easily 50% or
more of the total development cost.
• While a lot of new techniques have been
proposed, but they basically follow this
traditional V&V paradigm that emphasizes on
IV&V (Independent Verification and Validation)
Real-Time and Network-Centric V&V
V&V for Service-Oriented Computing (SOC)
• Service-oriented computing (SOC) and service-oriented
architecture (SOA) represent a new paradigm for
computing, and it will have dynamic discovery,
composition and dynamic omposition in real-time and at
runtime.
• These features need a new approach for V&V, CV&V
(Collaborative V&V) as V&V will need multiple parties to
collaborate and cooperate, and as new services will be
discovered and used in real time, V&V will be done in
real time.
• CV&V will be different from the traditional IV&V.
• Many mission-critical (embedded) systems need real-time V&V as
they involve dynamic reconfiguration. For example, combat aircrafts,
tanks, spaceships, manufacturing process control, and C2 systems.
Many of these systems also started to use service-oriented
architecture, e.g., FCS, and FORCEnet. In these systems, new code
is generated in real time.
• Currently, model V&V techniques (sponsored by DoD and NASA)
are available via neural networks and/or simulation.
• However, code generated also must be verified and validated in real
time and at runtime, and this is what we address.
• Computing trend
– Time sharing systems (one machine but multiple people);
– PCs (one machine for one person);
– Multiple machines for one person (Internet and PDAs); and
– Multiple machines for one mission (dynamic NCW C2 applications).
• Network-Centric Warfare (NCW)
– GIG-compliant (policy-driven computing)
– Service-Oriented Architecture (SOA) such as NCES,
GIG-ES, JBMC2, FCS, andFORCEnet.
– Survivable systems
• Rapid and adaptive acquisition and fielding for
NCW
– Rapid but reliable system engineering
– Modeling and simulation
– Analysis, Verification, and Validation
– Dynamic reconfiguration
We have been working on V&V issues in the
past including
– Testing techniques for OO
– Regression testing
– End-to-end integration testing
– Y2K testing such as Y2K windowing testing
– Completeness and consistency checking
– Distributed service-oriented simulation
– Model checker
– Policy specification, analysis, and enforcement
– Rapid and automated test case/script generation
– New test coverage (Swiss Cheese)
Overall Goal
• To support rapid development and evaluation of
Network-Centric Warfare (NCW) Command and
Control (C2) applications:
– Specification and analysis including system
engineering issues such as reliability, security, and
safety analyses
– Dynamic code generation in real time and at runtime
• Semiconductor manufacturing process control at Intel
• Not just code generation, but reliable and real-time code
generation with monitoring and V&V
– Real-time V&V
• Automated test case/script generation (Swiss Cheese and
Verification Patterns), model checking, simulation,
completeness and consistency checking
– Support policy-based computing (GIG)
• Policy specification, verification and validation, and
distributed enforcement
– Real-time distributed service-oriented
simulation
• Automated simulation code generation
– Real-time verification and validation of WS
(Web Services) in SOA
• Collaborative V&V, ranking of WS, test
cases/scripts, automated oracle establishment
– Code analysis and real-time reasoning
Dependable and Automated Software Development with RTV&V
Dynamic Verification and Distributed Simulation
Dynamic SOA Composition and Recomposition
• Rapid service-oriented system development.
• Design time and runtime code generation and dynamic
system reconfiguration at real-time without stopping the
system.
• Built-in runtime composition and reconfiguration
mechanism within the generated system.
• System semantics, composition and reconfiguration
Rules are represented uniformly by scenarios for easy
development. No need to learn multiple languages.
• Drag & Drop model-driven application development.
• Rapid system integration through automated service’s
meta-information extraction and dynamic binding.
Simulation Frameworks
Demo
• This demo will show that this new RTV2 approach is
feasible.
• The application is an embedded car that is controlled by
reconfigurable software.
• Once the software is changed, the code will be subjected
to the following V&V:
– Dynamic reconfiguration and automated code generation
– Real-time model checking
– Real-time simulation
– Real-time policy enforcement
• Initial configuration:
–When run into obstacle, DCS service transmit alternative routes directly to Rover controller. DCS picks the simplest route.
• Steps:
– Create application model.
– Configure initial system configuration, generate application code,deploy system.
– Start up dynamic composition and re-composition service.
– Once Rover controller detects obstacle, DCS chooses a route (verified by model checker, simulation, and policies) that couldcircumvent the obstacle base on its size and sends it back to Rover controller.
Model Checking Rover-Control Scenarios
• Before deployment, rover-control scenarios are checked to ensure correctness
• In the demo, we check a simple property: whether the rover arrives
at the destination following the scenarios
– Each move is modeled as either x x±1 or y y±1, depending on the
direction
– Let x, y be the current location, and xt, yt be the destination. We check
the assertion (x = xt)∧(y = yt) after the execution of a control scenario.
• The model checker is encapsulated as a web service
Input: a program with
• Peano arithmetic
• Sequence, branch, and loop
Output:
• “Pass” when no assertion fails
• A counterexample when any assertion fails.
A counterexample is an execution trace that witnesses the failure.
• Blade can check all temporal properties with universal quantifiers.
Embedded Car Policies
• Policy Types – Car must / must not reach a point
• Example
– Car must not reach the coordinate (2, 5)
– Car must / must not enter an area
• Example
– Car must not enter an area centered by (5, 2) with radius of 2
– Car must stay in an area from source / destination
• Example
– The distance between the source and car’s current coordinate must be <= 10
– Car must / must not move in a specified sequence
• Example – Car must not make a right turn right after a left turn
New V&V Paradigm
• RTV2 is different from IV&V.
• It is performed in real time and at runtime.
• This approach is designed to develop the nextgeneration
C2 systems.
• It has been experimented on several embedded
systems including an aircraft flight control.
• The system code and V&V (including simulation,
dynamic policy modification and enforcement,
test cases) code can be automatically generated
and reconfigured in real time.
• It uses a variety of new and existing V&V
techniques.
For More Information
• Blade model checker http://asusrl.eas.asu.edu/blade/
• Distributed service-oriented simulation: http://asusrl.eas.asu.edu/simulation/
• Embedded systems: http://asusrl.eas.asu.edu/EmbeddedExplorer/
• Web service testing: http://asusrl.eas.asu.edu/srlab/projects/webstrar/index.htm
• Policy specification, analysis and enforcement: http://asusrl.eas.asu.edu/psel/
• DCS or service dynamic reconfiguration: http://whoknows.eas.asu.edu/~wwsong/DCS.htm
Completeness and Consistency (C&C) Analysis
• Perform completeness analysis to identify all the missing system specifications.• Identify and minimize the set of scenarios that need to be updated to make the system complete and robust.
• The minimization algorithm is much more efficient than similar algorithms like Quine-McCluskey algorithm.
• The whole process is automated in a GUI-based C&C analysis tool.
• The proposed techniques have been proved to be effective in solving large applications including:
• Several large real-time distributed command-and-control NCW (Network-Centric Warfare) systems for the US Department of Defense (DoD);
• A large real-time mission-critical process control for semiconductor manufacturing for Intel corporation; and
• A large real-time high-availability communication processor for Motorola.• Perform completeness analysis to identify all the missing system specifications.
• Identify and minimize the set of scenarios that need to be updated to make the system complete and robust.
• The minimization algorithm is much more efficient than similar algorithms like Quine-McCluskey algorithm.
• The whole process is automated in a GUI-based C&C analysis tool.
• The proposed techniques have been proved to be effective in solving large applications including:
• Several large real-time distributed command-and-control NCW (Network-Centric Warfare) systems for the US Department of Defense (DoD);
• A large real-time mission-critical process control for semiconductor manufacturing for Intel corporation; and
• A large real-time high-availability communication processor.
New Test Case Generation based on the Swiss Cheese (SC) Model
• A systematic approach to generate and select the most powerful test
data that can detect faults in the software.
• The two selection criteria: Hamming distance (HD) and Boundary
Degree (BD) are based on the topology structure of the Boolean
expression format system specifications.
• Allow the users to generate test data for positive testing or negative
testing or both.
• Provide GUI-based tool support which can automatically generate
most-error prone test data and draw corresponding SC diagrams.
• SC Model has been proved to be effective in generating test data for
large applications including:
• Stock Web service
• A large real-time mission-critical process control for semiconductor
manufacturing for Intel corporation; and
• A large real-time high-availability communication processor .
Swiss Cheese (SC) Model for Software Testing Based on Boolean Expressions
• A systematic approach to generate and select the most powerful test
data that can detect faults in the software.
• The two selection criteria: Hamming distance (HD) and Boundary
Degree (BD) are based on the topology structure of the Boolean
expression format system specifications.
• Allow the users to generate test data for positive testing or negative
testing or both.
• Provide GUI-based tool support which can automatically generate
most-error prone test data and draw corresponding SC diagrams.
• SC Model has been proved to be effective in generating test data for
large applications including:
• Stock Web service
• A large real-time mission-critical process control for semiconductor
manufacturing for Intel corporation; and
• A large real-time high-availability communication processor.
Back to ASU Software Research Lab
Last update: May 11, 2005 |