Visible to the public Static-Dynamic Analysis of Security Metrics for Cyber-Physical Systems - July 2015Conflict Detection Enabled

Submitted by amyclay on Wed, 07/08/2015 - 4:46pm

Public Audience
Purpose: To highlight project progress. Information is generally at a higher level which is accessible to the interested public. All information contained in the report (regions 1-3) is a Government Deliverable/CDRL.

PI(s): Sayan Mitra

Co-PI(s): Geir Dullerud and Swarat Chaudhuri (Rice University)

HARD PROBLEM(S) ADDRESSED
This refers to Hard Problems, released November 2012.

  • Scalability and composability
  • Predictive security metrics

Our mathematical framework and algorithms will provide quantitative measures of security metrics in a model-based design environment, with respect to different adversary classes.

PUBLICATIONS
Papers published in this quarter as a result of this research. Include title, author(s), venue published/presented, and a short description or abstract. Identify which hard problem(s) the publication addressed. Papers that have not yet been published should be reported in region 2 below.

[1] Simulation-based Verification of Cardiac Pacemakers with Guaranteed Coverage. Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, and Marta Kwiatkowska. Appeared in a Special Issue of the IEEE Design and Test, June 2015. DOI 10.1109/MDAT.2015.2448543

ACCOMPLISHMENT HIGHLIGHTS

  • Our simulation-based formal analysis approaches have gained momentum. The IEEE Design and Test paper mentioned above shows that this approach can be used to analyze models of medical devices like pacemakers together with relevant abstractions of physiology. In another related paper, we show that the approaches can handle challenge problems coming from the automotive industry. That paper received the Robert Bosch sponsored best verification result award at the ARCH workshop of CPSWeek.
  • Our inductive synthesis algorithm is currently under review. Zhenqi Huang attended the Excape Synthesis Summer School at MIT. This summer we are looking to apply these approaches to realistic drone models for automatic synthesis.
Groups: