
NSF Org: |
CNS Division Of Computer and Network Systems |
Recipient: |
|
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 2012 = $76,969.00 FY 2013 = $164,801.00 FY 2014 = $24,363.00 FY 2015 = $88,185.00 |
History of Investigator: |
|
Recipient Sponsored Research Office: |
5000 FORBES AVE PITTSBURGH PA US 15213-3890 (412)268-8746 |
Sponsor Congressional District: |
|
Primary Place of Performance: |
5000 FORBES AVE PITTSBURGH PA US 15213-3890 |
Primary Place of
Performance Congressional District: |
|
Unique Entity Identifier (UEI): |
|
Parent UEI: |
|
NSF Program(s): |
CSR-Computer Systems Research, Software & Hardware Foundation |
Primary Program Source: |
01001213DB NSF RESEARCH & RELATED ACTIVIT 01001314DB NSF RESEARCH & RELATED ACTIVIT 01001415DB NSF RESEARCH & RELATED ACTIVIT 01001516DB NSF RESEARCH & RELATED ACTIVIT |
Program Reference Code(s): |
|
Program Element Code(s): |
|
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.
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.