Principal Investigator

André Platzer

Status

Completed

Start Date

Jan. 1, 2014

End Date

Jan. 1, 2015

Project Type

Research Advanced

Grant Program

MAP-21 TSET - Tier 1 (2012 - 2016)

Grant Cycle

2015 TSET UTC

Visibility

Public

Abstract

Safety-critical traffic and automotive systems are becoming increasingly dependent on complex interactions with computers. Safety systems, such as adaptive cruise control, emergency braking and collision mitigation are becoming household terms, as family cars are equipped and sold with these devices. However, with this increased complexity, it is far more challenging to ensure the safe and accurate functioning of these devices, especially as an increasing number of them begin to interact on our roadways in a wide range of situations. Our research focuses on ensuring that these and other systems operate safely in all situations, even in those that are not conceived by the designers of the systems. To tackle this issue, we apply formal verification techniques, which allow us to either produce a conclusive proof that the systems is safe in all situations, or provide a counter example. However, these methods are only useful if they are powerful and robust enough to verify the computers, which actually control our cars. To this end, we have developed several collaborations with people outside our field to ensure that the methods and tools we develop are increasingly applicable and useful. One such collaboration is with researchers in the Engineering department at Carnegie Mellon University. Together we are investigating how to create the right abstractions to translate systems, which are currently too complex to prove directly into provably safe systems, without lessening the strength of our safety guarantees on the original system. Despite the remarkable progress in automating formal verification of hybrid systems, the construction of proofs of complex systems often requires nontrivial human guidance, since hybrid systems verification tools solve undecidable problems. It is, thus, not uncommon for development and verification teams to consist of many players with diverse expertise. We introduced a verification-driven engineering toolset that makes it easier to tackle large-scale verification tasks.     

Description

In order to ultimately enable domain experts, such as traffic engineers, to ensure safety by formal verification, we develop user-friendly modeling and verification tools including tutorial and course material. The KeYmaera tool is a freely available, hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. System models for KeYmaera can be created with Sphinx, a freely available modeling tool for hybrid programs. Through Sphinx, domain experts can create graphical and textual models of hybrid systems that are suitable for formal verification in KeYmaera (details in J. Mathematics in Computer Science). In this effort, we collaborated with Grant Olney Passmore. KeYmaera and Sphinx support simulation of those models to help domain experts gain intuition about the behavior of their models. Proper safe developments of transportation system designs are accompanied by a proof of correctness. Since the inherent complexities of those systems practically mandate iterative development, frequent changes of models are standard practice, but require re-verification of the resulting models after every change. To overcome this issue, we developed proof-aware refactorings that transform system models and maintain correctness proofs. We developed and taught “Foundations of cyber-physical systems” (FCPS), an undergraduate course on the formal verification of cyber-physical systems. The course introduces formal verification techniques and hybrid system modeling, with a special focus on autonomous robots as a running example throughout the course. The course was offered during the Fall 2013 term, and is offered again in the Fall 2014 term. The course material includes lecture notes, lab assignments, homework assignments, and YouTube demonstrations for new KeYmaera users. In addition to completing the publicly available course material, Carnegie Mellon FCPS students completed an end-of-term verification project. Three of these end-of-term projects were presented at Carnegie Mellon's Undergraduate Research Symposium, resulting in one award. Short versions of this course were presented to graduate students and faculty at Universidade do Minho and Ens de Lyon.

Timeline

-

Strategic Description / RD&T

Deployment Plan

-

Expected Outcomes/Impacts

Impact in other Disciplines: Much of our research has resulted from cross-disciplinary collaborations. We have developed several collaborations with people outside our field to ensure that the methods and tools we develop are increasingly applicable and useful. One such collaboration is with researchers in the Engineering department at Carnegie Mellon University on abstraction and translation of complex systems into provably safe systems. Another collaboration is with Johannes Kepler University Linz, Department of Cooperative Information Systems. In this collaboration, we investigate how to integrate safe traffic control measures into an intermodal traffic situational awareness software framework for traffic control centers. These efforts are expected to contribute to traffic information system engineering, in order to increase safety and trustworthiness of information systems in the traffic control domain.

Expected Outputs

TRID

Individuals Involved

Email	Name	Affiliation	Role	Position
aplatzer@cs.cmu.edu	Platzer, André	CS	PI	Faculty - Adjunct

Budget

Amount of UTC Funds Awarded

$98420.00

Total Project Budget (from all funding sources)

$98420.00

Documents

Type	Name	Uploaded
Final Report	Proving_Autonomous_Vehicle_and_Advanced_Driver_AfRu7K3.pdf	June 18, 2018, 5:22 a.m.

Match Sources

No match sources!

Partners

No partners!