Skip directly to content

Minimize RSR Award Detail

Research Spending & Results

Award Detail

Awardee:KANSAS STATE UNIVERSITY
Doing Business As Name:Kansas State University
PD/PI:
  • Pavithra Prabhakar
  • (785) 532-6350
  • pprabhakar@ksu.edu
Award Date:01/05/2016
Estimated Total Award Amount: $ 446,681
Funds Obligated to Date: $ 150,668
  • FY 2016=$150,668
Start Date:01/15/2016
End Date:12/31/2020
Transaction Type:Grant
Agency:NSF
Awarding Agency Code:4900
Funding Agency Code:4900
CFDA Number:47.070
Primary Program Source:040100 NSF RESEARCH & RELATED ACTIVIT
Award Title or Description:CAREER:Robust Verification of Cyber-Physical Systems
Federal Award ID Number:1552668
DUNS ID:929773554
Parent DUNS ID:041146432
Program:SOFTWARE & HARDWARE FOUNDATION
Program Officer:
  • Nina Amla
  • (703) 292-8910
  • namla@nsf.gov

Awardee Location

Street:2 FAIRCHILD HALL
City:Manhattan
State:KS
ZIP:66506-1100
County:Manhattan
Country:US
Awardee Cong. District:01

Primary Place of Performance

Organization Name:Kansas State University
Street:2 Fairchild
City:Manhattan
State:KS
ZIP:66506-1103
County:Manhattan
Country:US
Cong. District:01

Abstract at Time of Award

Cyber-physical systems (CPSs) have become pervasive in the modern society, enabling transformative applications in the transportation, healthcare and energy sectors. However, the reliable development of CPSs remains an outstanding challenge. At the design level, hybrid systems theory provides a rich set of techniques and tools for ensuring correctness of high level functional properties such as safety and liveness. Current analysis techniques at the implementation level focus primarily on detecting low level runtime errors such as buffer overflows and divide by zero. A holistic approach to verifying functional specifications will considerably enhance the reliability scenario of CPSs development. This project investigates a robust verification methodology that guarantees functional correctness of the implementation by a "deeper" analysis on the design. More precisely, robust verification not only ensures that a design satisfies a given specification, but that small perturbations in the design still satisfy the specification. The perturbations on the design account for the deviations in the implementation with respect to the actual system. The proposed research investigates new foundations, abstractions and verification algorithms for robust analysis, in light of novel quantitative and/or topological aspects of robustness. In addition, prototype tools are developed to enable practical application and evaluation. The successful completion of the research will advance the knowledge in the fields of formal methods and hybrid control systems by leveraging ideas from control theory, dynamical systems theory, optimization theory and satisfiability modulo theory. New cross-disciplinary courses at the undergraduate and graduate levels in hybrid control system design and analysis will be developed and taught. Activities for pre-college students involving programming with physical systems will be conducted towards increasing their interest in STEM related careers. Undergraduates, especially those from minority and underrepresented groups, will be recruited and mentored through involvement in research and outreach activities. The success of this research will force a quantum jump in the existing verification methodologies for CPSs, in particular, in the domains of automotive and aerospace systems, by bridging the gap in the analyses at the design and implementation phases.

For specific questions or comments about this information including the NSF Project Outcomes Report, contact us.