Difference between revisions of "2005 MURI White Paper"

From MurrayWiki
Jump to: navigation, search
(=Proposed technical approach=)
Line 1: Line 1:
=== cover letter (optional) ===
+
== Cover letter (optional) ==
 
* Not sure what to put here.  Perhaps description of team?  Assume this won't be read by anyone but program manager.
 
* Not sure what to put here.  Perhaps description of team?  Assume this won't be read by anyone but program manager.
  
=== Cover Page ===
+
== Cover Page ==
 
* The cover page shall be labeled “PROPOSAL WHITE PAPER” and shall include the BAA number 05-017, proposed title, and proposer’s technical point of contact, with telephone number, facsimile number, and email address
 
* The cover page shall be labeled “PROPOSAL WHITE PAPER” and shall include the BAA number 05-017, proposed title, and proposer’s technical point of contact, with telephone number, facsimile number, and email address
  
=== Identification of the research and issues ===
+
== Identification of the research and issues ==
  
 
We propose to develop a mathematical language for specification, design and verification of distributed, embedded systems that provides an analyzable framework for robust performance.
 
We propose to develop a mathematical language for specification, design and verification of distributed, embedded systems that provides an analyzable framework for robust performance.
Line 15: Line 15:
 
# ''Demonstrate the utility of these methods on problems in network centric environments.''  We will make use of two testbeds at Caltech for this purpose - the Caltech Multi-Vehicle Wireless Testbed (MVWT) and "Alice", our 2005 DARPA Grand Challenge entry.  Alice provides a sophisticated embedded system environment that includes 5 Gb/s raw data rates from sensors, 12 high speed processing cores linked by 1 Gb/s ethernet and a complex set of tasks and environments for autonomous operations.  The MVWT offers a simpler dynamic and computational environment, but allows cooperative control of multiple vehicles operating in a dynamic, uncertain and adversarial environment.  In each case we propose to develop a collection of primitive operations which can be used to "program" the systems and provide automatically verified code that satisfies a given performance specification.
 
# ''Demonstrate the utility of these methods on problems in network centric environments.''  We will make use of two testbeds at Caltech for this purpose - the Caltech Multi-Vehicle Wireless Testbed (MVWT) and "Alice", our 2005 DARPA Grand Challenge entry.  Alice provides a sophisticated embedded system environment that includes 5 Gb/s raw data rates from sensors, 12 high speed processing cores linked by 1 Gb/s ethernet and a complex set of tasks and environments for autonomous operations.  The MVWT offers a simpler dynamic and computational environment, but allows cooperative control of multiple vehicles operating in a dynamic, uncertain and adversarial environment.  In each case we propose to develop a collection of primitive operations which can be used to "program" the systems and provide automatically verified code that satisfies a given performance specification.
  
=== Proposed technical approach ===
+
== Proposed technical approach ==
  
==== Background (Richard; 1/2 page) ====
+
=== Background (Richard; 1/2 page) ===
  
==== Sum of Squares Techniques (Pablo, with John; 1 page) ====
+
=== Sum of Squares Techniques (Pablo, with John; 1 page) ===
 
* Provide a short (1-2 paragraph) background on current state of SoS
 
* Provide a short (1-2 paragraph) background on current state of SoS
 
* Talk about what is lacking from current approach
 
* Talk about what is lacking from current approach
Line 29: Line 29:
 
* Give some insights into how we plan to approach this and desired results
 
* Give some insights into how we plan to approach this and desired results
  
==== Testbeds (Richard; 1/2 page) ====
+
=== Testbeds (Richard; 1/2 page) ===
  
===== MVWT =====
+
==== MVWT ====
 
* Talk about development of a language that allows us to put together complex tasks and make sure they satisfy the spec
 
* Talk about development of a language that allows us to put together complex tasks and make sure they satisfy the spec
  
===== Alice =====
+
==== Alice ====
 
* Not sure whether we should really include this
 
* Not sure whether we should really include this
  
=== Potential impact on DoD capabities ===
+
== Potential impact on DoD capabities ==
  
=== Potential team and management plan ===
+
== Potential team and management plan ==
  
=== Summary of estimated costs ===
+
== Summary of estimated costs ==
 
* $1M/year
 
* $1M/year
  
=== Curriculum vitae of key investigators ===
+
== Curriculum vitae of key investigators ==
  
 
==== Mani Chandy ====
 
==== Mani Chandy ====

Revision as of 16:32, 26 July 2005

Cover letter (optional)

  • Not sure what to put here. Perhaps description of team? Assume this won't be read by anyone but program manager.

Cover Page

  • The cover page shall be labeled “PROPOSAL WHITE PAPER” and shall include the BAA number 05-017, proposed title, and proposer’s technical point of contact, with telephone number, facsimile number, and email address

Identification of the research and issues

We propose to develop a mathematical language for specification, design and verification of distributed, embedded systems that provides an analyzable framework for robust performance.

Our specific goals for this MURI are to:

  1. Develop common mathematical framework for analyzing distributed, hybrid systems. This framework will be able to handle a combination of continuous dynamics and temporal logic, building on our previous work in analysis of hybrid dynamical systems. This will require a significant extension of current work to include temporal logic and distributed computing. In addition, we believe that it will be important to include stochatic systems, extending work such as SoSTools to include probabalistic analysis.
  2. Extend ideas from distributed/parallel computing to apply to dynamical systems. Concepts such as fairness, safety, progress and concurrency are not strongly linked with concepts such as dynamics, stability and performance in embedded systems. We plan to extend tools in distributed computing to allow for dynamic changes in behavior and provide methods for analyzing robustness to such changes. This includes incremental changes (evolution of the dynamic state), large changes (changes in mode or failure of a component) and probabalistic changes (noise, disturbances and other stochastic uncertainties).
  3. Move the handoff between handcrafted proofs and formal methods further upstream. A major theme of our work will be to show how to take currently handcrafted proofs and formal methods for verification and validation of embedded systems and move them to higher levels of complexity and abstraction. This will enable the design of increasingly complex systems without the need for huge amounts of iteration and Monte Carlo analysis to verify performance.
  4. Demonstrate the utility of these methods on problems in network centric environments. We will make use of two testbeds at Caltech for this purpose - the Caltech Multi-Vehicle Wireless Testbed (MVWT) and "Alice", our 2005 DARPA Grand Challenge entry. Alice provides a sophisticated embedded system environment that includes 5 Gb/s raw data rates from sensors, 12 high speed processing cores linked by 1 Gb/s ethernet and a complex set of tasks and environments for autonomous operations. The MVWT offers a simpler dynamic and computational environment, but allows cooperative control of multiple vehicles operating in a dynamic, uncertain and adversarial environment. In each case we propose to develop a collection of primitive operations which can be used to "program" the systems and provide automatically verified code that satisfies a given performance specification.

Proposed technical approach

Background (Richard; 1/2 page)

Sum of Squares Techniques (Pablo, with John; 1 page)

  • Provide a short (1-2 paragraph) background on current state of SoS
  • Talk about what is lacking from current approach
  • Give some insights into how we plan to approach this and desired results

Specification and Programming Languages (Eric, with Mani; 1 page)

  • Provide a short (1-2 paragraph) background on current state (CCL, unity, graph grammers, etc)
  • Talk about what is lacking from current approach
  • Give some insights into how we plan to approach this and desired results

Testbeds (Richard; 1/2 page)

MVWT

  • Talk about development of a language that allows us to put together complex tasks and make sure they satisfy the spec

Alice

  • Not sure whether we should really include this

Potential impact on DoD capabities

Potential team and management plan

Summary of estimated costs

  • $1M/year

Curriculum vitae of key investigators

Mani Chandy

John Doyle

Eric Klavins

Richard Murray (PI)

Pablo Parrilo