Phoenix Project

Introduction to Phoenix

"Phoenix is the code name for a software optimization and analysis framework that is the basis for all future Microsoft compiler technologies. The Phoenix framework is an extensible system that can be adapted to read and write binaries and MSIL assemblies and represent the input files in an IR, which can be analyzed and manipulated by applications by using the Phoenix API. The code can then be written in binary or JITable form for execution."

For more information, please visit this website.

Introduction to Hot Patching Project

Patching technologies are commonly applied to improve the dependability of software after release. This paper proposes an autonomous hot patching (AHP) framework to fully automate the reasoning for the causes of failures, and to patch the binary code of Web-based applications. AHP admits the hardness for rooting out all faults before product release, and autonomously patches problems of application programs. By directly operating on binary code, AHP is universal to virtually all applications. A promising application of AHP is to shortcut the remote maintenance center (RMC) and hence to reduce the turn around time for patches.

In our hot patching project, we make use of Microsoft's Phoneix RDK as our code instrumentation tool to do hot pathing.

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

RTV&V

Feedback Control in RTV&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.

Trends Observed

• 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

History

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

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