| NSF Org: |
CNS Division Of Computer and Network Systems |
| Recipient: |
|
| Initial Amendment Date: | September 11, 2009 |
| Latest Amendment Date: | September 11, 2009 |
| Award Number: | 0931985 |
| Award Instrument: | Standard Grant |
| Program Manager: |
David Corman
CNS Division Of Computer and Network Systems CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | September 1, 2009 |
| End Date: | August 31, 2014 (Estimated) |
| Total Intended Award Amount: | $550,000.00 |
| Total Awarded Amount to Date: | $550,000.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
5000 FORBES AVE PITTSBURGH PA US 15213-3815 (412)268-8746 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
5000 FORBES AVE PITTSBURGH PA US 15213-3815 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Information Technology Researc |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
CPS: Small: Compositionality and Reconfiguration for Distributed Hybrid Systems
The objective of this research is to address fundamental challenges in the verification and analysis of reconfigurable distributed hybrid control systems. These occur frequently whenever control decisions for a continuous plant depend on the actions and state of other participants. They are not supported by verification technology today. The approach advocated here is to develop strictly compositional proof-based verification techniques to close this analytic gap in cyber-physical system design and to overcome scalability issues. This project develops techniques using symbolic invariants for differential equations to address the analytic gap between nonlinear applications and present verification techniques for linear dynamics.
This project aims at transformative research changing the scope of systems that can be analyzed. The proposed research develops a compositional proof-based approach to hybrid systems verification in contrast to the dominant automata-based verification approaches. It represents a major improvement addressing the challenges of composition, reconfiguration, and nonlinearity in system models.
The proposed research has significant applications in the verification of safety-critical properties in next generation cyber-physical systems. This includes distributed car control, robotic swarms, and unmanned aerial vehicle cooperation schemes to full collision avoidance protocols for multiple aircraft. Analysis tools for distributed hybrid systems have a broad range of applications of varying degrees of safety-criticality, validation cost, and operative risk. Analytic techniques that find bugs or ensure correct functioning can save lives and money, and therefore are likely to have substantial economic and societal impact.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external
site maintained by the publisher. Some full text articles may not yet be available without a
charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from
this site.
Please report errors in award information by writing to: awardsearch@nsf.gov.
