Award Abstract # 0931985
CPS: Small: Compositionality and Reconfiguration for Distributed Hybrid Systems

NSF Org: CNS
Division Of Computer and Network Systems
Recipient: CARNEGIE MELLON UNIVERSITY
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: FY 2009 = $550,000.00
History of Investigator:
  • Andre Platzer (Principal Investigator)
    aplatzer@cs.cmu.edu
  • Edmund Clarke (Co-Principal Investigator)
Recipient Sponsored Research Office: Carnegie-Mellon University
5000 FORBES AVE
PITTSBURGH
PA  US  15213-3815
(412)268-8746
Sponsor Congressional District: 12
Primary Place of Performance: Carnegie-Mellon University
5000 FORBES AVE
PITTSBURGH
PA  US  15213-3815
Primary Place of Performance
Congressional District:
12
Unique Entity Identifier (UEI): U3NKNFLNQ613
Parent UEI: U3NKNFLNQ613
NSF Program(s): Information Technology Researc
Primary Program Source: 01000910DB NSF RESEARCH & RELATED ACTIVIT
Program Reference Code(s): 7751, 7918, 9216, 9218, HPCC
Program Element Code(s): 164000
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.

André Platzer "A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems." Logical Methods in Computer Science , v.8 , 2012 http://www.lmcs-online.org/ojs/viewarticle.php?id=820
André Platzer "The structure of differential invariants and differential cut elimination." Logical Methods in Computer Science , v.8 , 2012 http://www.lmcs-online.org/ojs/viewarticle.php?id=860
Stefan Mitsch and Grant Olney Passmore and Andr{\'e} Platzer "Collaborative Verification-Driven Engineering of Hybrid Systems" Mathematics in Computer Science , v.8 , 2014 , p.71-97 10.1007/s11786-014-0176-y

Please report errors in award information by writing to: awardsearch@nsf.gov.

Print this page

Back to Top of page