Award Abstract # 1054246
CAREER: Logical Foundations of Cyber-Physical Systems

NSF Org: CNS
Division Of Computer and Network Systems
Recipient: CARNEGIE MELLON UNIVERSITY
Initial Amendment Date: January 25, 2011
Latest Amendment Date: May 15, 2015
Award Number: 1054246
Award Instrument: Continuing Grant
Program Manager: Marilyn McClure
mmcclure@nsf.gov
 (703)292-5197
CNS
 Division Of Computer and Network Systems
CSE
 Directorate for Computer and Information Science and Engineering
Start Date: February 1, 2011
End Date: January 31, 2018 (Estimated)
Total Intended Award Amount: $403,532.00
Total Awarded Amount to Date: $427,895.00
Funds Obligated to Date: FY 2011 = $73,577.00
FY 2012 = $76,969.00

FY 2013 = $164,801.00

FY 2014 = $24,363.00

FY 2015 = $88,185.00
History of Investigator:
  • Andre Platzer (Principal Investigator)
    aplatzer@cs.cmu.edu
Recipient Sponsored Research Office: Carnegie-Mellon University
5000 FORBES AVE
PITTSBURGH
PA  US  15213-3890
(412)268-8746
Sponsor Congressional District: 12
Primary Place of Performance: Carnegie-Mellon University
5000 FORBES AVE
PITTSBURGH
PA  US  15213-3890
Primary Place of Performance
Congressional District:
12
Unique Entity Identifier (UEI): U3NKNFLNQ613
Parent UEI: U3NKNFLNQ613
NSF Program(s): CSR-Computer Systems Research,
Software & Hardware Foundation
Primary Program Source: 01001112DB NSF RESEARCH & RELATED ACTIVIT
01001213DB NSF RESEARCH & RELATED ACTIVIT

01001314DB NSF RESEARCH & RELATED ACTIVIT

01001415DB NSF RESEARCH & RELATED ACTIVIT

01001516DB NSF RESEARCH & RELATED ACTIVIT
Program Reference Code(s): 1045, 1187
Program Element Code(s): 735400, 779800
Award Agency Code: 4900
Fund Agency Code: 4900
Assistance Listing Number(s): 47.070

ABSTRACT

This project seeks to develop logical foundations for cyber-physical systems (CPS), i.e., systems that combine cyber aspects such as communication and computer control with physical aspects such as movement in space. CPS applications abound. Ensuring their correct functioning, however, is a serious challenge. Scientists and engineers need analytic tools to understand and predict the behavior of their systems. This is the key to designing smart and reliable control. By providing such analytic foundations, this project addresses an intellectual grand challenge that has substantial scientific, economical, societal, and educational impact arising from the benefits of improved CPS analysis and design. In order to tame their complexity, this project studies CPS as multi-dynamical systems, i.e., in terms of the elementary dynamical aspects of their parts.

Multi-billion dollar industries spend 50% of the development cost on control software design and testing. This cannot be sustained any longer. The foundations of computer science have revolutionized our society. We need even stronger foundations when software interacts with the physical world. Multi-dynamical systems concepts provide a unifying principle for education and enable students to focus on one dynamical aspect at a time without missing the big picture. They overcome the divide between computer science and engineering that keeps causing irreconcilable differences among design teams. This project develops cross-departmental graduate/undergraduate courses on Mathematical Foundations of CPS as prime examples of STEM integration. Long-term goals include a K-12 outreach that inspires young people to pursue science careers through an early exposure to both mathematical beauty and exciting societal challenges. CPS foundations excel in demonstrating the paramount importance of discrete and continuous mathematics, not as separate disciplines, but well-integrated.

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.

(Showing: 1 - 10 of 20)
Andre Platzer "A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems." Logical Methods in Computer Science , v.8 , 2012 , p.1-44
Andre Platzer "A Complete Uniform Substitution Calculus for Differential Dynamic Logic" J. Autom. Reas. , 2016 10.1007/s10817-016-9385-1
Andre Platzer "A Complete Uniform Substitution Calculus for Differential Dynamic Logic" J. Autom. Reas. , v.59 , 2017 , p.219-265 10.1007/s10817-016-9385-1
Andre Platzer "Analog and Hybrid Computation: Dynamical Systems and Programming Languages" Bulletin of the {EATCS} , v.114 , 2014 http://bulletin.eatcs.org/index.php/beatcs/article/viewFile/292/274
Andre Platzer "Differential Game Logic" ACM TOCL , v.17 , 2015 , p.1 10.1145/2817824
Andre Platzer "Differential Hybrid Games" ACM Trans. Comput. Log. , v.18 , 2017 , p.19:1 10.1145/3091123
Andre Platzer "The structure of differential invariants and differential cut elimination" Logical Methods in Computer Science , v.8 , 2012 , p.1-38
Jan-David Quesel and Stefan Mitsch and Sarah Loos and Nikos Arechiga and Andre Platzer "How to Model and Prove Hybrid Systems with {KeYmaera}: A Tutorial on Safety" STTT , v.18 , 2016 , p.67-91 10.1007/s10009-015-0367-0
Jan-David Quesel and Stefan Mitsch and Sarah Loos and Nikos Arechiga and Andre Platzer "How to Prove Complex Properties of Hybrid Systems with KeYmaera: A Tutorial" STTT , 2015
Jean-Baptiste Jeannin and Khalil Ghorbal and Yanni Kouskoulas and Aurora Schmidt and Ryan Gardner and Stefan Mitsch and Andre Platzer "A Formally Verified Hybrid System for Safe Advisories in the Next-generation Airborne Collision Avoidance System" STTT , 2016 10.1007/s10009-016-0434-1
Jean-Baptiste Jeannin and Khalil Ghorbal and Yanni Kouskoulas and Aurora Schmidt and Ryan Gardner and Stefan Mitsch and Andre Platzer "A Formally Verified Hybrid System for Safe Advisories in the Next-generation Airborne Collision Avoidance System" STTT , v.19 , 2017 , p.717-741 10.1007/s10009-016-0434-1
(Showing: 1 - 10 of 20)

PROJECT OUTCOMES REPORT

Disclaimer

This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.

Cyber-physical systems (CPS) combine cyber aspects such as communication and computer control with physical aspects such as movement in space, which arise frequently in many safety-critical application domains, including aviation, automotive, railway, and robotics. But how can we ensure that these systems are guaranteed to meet their design goals, e.g., that an aircraft will not crash into another one? Because of the impact that they can have on the real world, CPSs deserve nothing less than proof as safety evidence.


This CAREER project has been pursuing the most fascinating aspects of cyber-physical systems. In order to develop the principles for CPS proofs, this project went all the way down to identify the very atoms of reasoning for CPSs and emerged with an unshakably strong analytic foundation. The project then built its way up from this logical foundation in order to fundamentally characterize what is provable in the universe of cyber-physical systems. The resulting proof techniques provide comprehensive safety guarantees for mathematical models of the system. Since the relationship of real systems to their models can be elusive, logic also provides fundamental transfer principles that generalize safety results about models to CPS implementations by combining offline safety proof with online monitoring proof. These transfer principles were subsequently exploited to compile safe CPS models to safe CPS control executables by proof.


The findings of this project are disseminated in the undergraduate textbook on Logical Foundations of Cyber-Physical Systems. They are implemented in the KeYmaera X proof tool and are being used to improve the safety of the Federal Aviation Authority's Next-generation Airborne Collision Avoidance System ACAS X, in whose earlier versions KeYmaera X identified almost a billion counterexamples. They also led to safer designs of Positive Train Control, identified safe obstacle avoidance for ground robots, and improved the safety of a surgical robot controller.


Logical foundations make a big difference for CPSs, certainly for understanding the principles of CPS, but also in real applications like the FAA's ACAS X. Lessons from centuries of logic and foundations research can have a huge impact on advancing CPS. Yet, conversely, the questions that CPS pose can have an equally significant impact on advancing logic. CPSs serve as a catalytic integrator for other sciences, because they benefit from combining numerous exciting areas of logic, mathematics, computer science, and engineering that previously seemed unrelated. The mix of enabling strong analytic foundations with the need for practical advances of rigorous reasoning and the significance of its applications, as well as its fruitful interactions with many other sciences, make cyber-physical systems an ideal field for compelling and rewarding research that has only just begun. Numerous wonders remain yet to be discovered, fueled by the successes of this project.


While CPSs are widely appreciated for their broad range of application domains (e.g., automotive, aerospace, medical, transportation, civil engineering, materials, chemistry, energy), the goal of this CAREER project was to identify the common foundational core that constitutes the true essence of CPSs and their reasoning principles to serve as the simultaneous mathematical basis for all those applications. The foundations of digital computer science have revolutionized how systems are designed and our whole society works. We need even stronger foundations when software reaches out into our physical world.


Last Modified: 04/22/2018
Modified by: Andre Platzer

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

Print this page

Back to Top of page