High-Assurance Cyber-Physical System Design: Formal Foundations and Design Tools

Friday, March 2, 2018, 11:00 am - 12:00 pm PSTiCal
11th floor large conference room
This event is open to the public.
AI Seminar
Pierluigi Nuzzo, USC
Video Recording:

Safety-critical cyber-physical systems pose several design and verification challenges. The design space is often too large and heterogeneous to be efficiently explored with strong guarantees of correctness, dependability, and compliance with regulations. Requirement-management tools are still predominantly centered on text-based languages, which creates opportunities for ambiguities and potential conflicts. Poorly inter-operable domain-specific languages and tools make it hard to combine the results of different analysis or synthesis methods. Assessing system correctness is then left to lengthy simulations and prototype tests later in the design process, which may yield implementations that are inefficient and sometimes do not even satisfy the requirements.

This talk introduces a path towards an integrated, formal framework for the design of complex systems that can address the above challenges. The pillars of the framework are contracts, mathematical objects that model the interface between components in a design, and a satisfiability modulo convex programming (SMC) technique that can efficiently reason about the interaction between discrete and continuous models. Contracts enable modular and hierarchical system development based on formal notions of composition, abstraction, and refinement.  SMC integrates satisfiability (SAT) solving and convex programming to efficiently reason about Boolean and convex constraints at the same time. I illustrate their effectiveness on design examples inspired by aircraft electric power distribution networks, system state reconstruction under sensor attack, and robot motion planning.


Pierluigi Nuzzo is an Assistant Professor at the Department of Electrical Engineering of the University of Southern California, Los Angeles. He received the Ph.D. in Electrical Engineering and Computer Sciences from the University  of California at Berkeley and an M.Sc.  degree in Electrical Engineering from the University of Pisa and the Sant'Anna School of Advanced Studies, Pisa, Italy. Pierluigi’s research interests include methodologies and tools for the design of cyber-physical systems and mixed-signal systems; contracts, interfaces, and compositional methods for embedded system design and requirement engineering; the application of automated formal methods and optimization theory to problems in embedded and cyber-physical systems and electronic design automation. He was a recipient of the Best Submission in the Design Automation   Conference   (DAC)   and   International   Solid-State   Circuits   Conference   (ISSCC)   Design Competition in 2006, and the Best  Paper Award from the  International Conference on Cyber-Physical Systems (ICCPS) in 2016. His awards and honors also include the IBM Ph.D. Fellowship in 2012 and 2014 and the U.C. Berkeley David J. Sakrison Memorial Prize in 2016 for his doctoral research.

« Return to Upcoming Events