Events Calendar

Electrical Engineering Seminar

Speaker: Pierluigi Nuzzo, UC Berkeley

Talk Title: When Logic Meets Physics: Compositional Design of Cyber-Physical Systems Using Contracts

Abstract: The realization of large and complex cyber-physical systems (such as “smart” transportation, energy, security, and health-care systems) is creating design and verification challenges, which will soon become insurmountable with the current engineering practices. In this talk, I introduce a design methodology that addresses the complexity and heterogeneity of these systems by using assume-guarantee contracts to formalize the design process and enable the realization of system architectures and control algorithms in a hierarchical and compositional way.
In the proposed methodology, the design is carried out as a sequence of refinement steps from a high-level specification to an implementation built out of a library of components at the lower level. Top-level system requirements are represented as contracts, by leveraging a set of formal languages, including mixed integer-linear constraints and temporal logic, to allow for requirement analysis and early detection of inconsistencies. Top-level contracts are then refined to achieve independent implementation of system architecture and control algorithm, by combining synthesis from requirements, optimization and simulation-based design space exploration methods. I show how key analysis tasks, such as refinement checking, can indeed be made more efficient when a system is described based on a pre-characterized library of components and contracts. Moreover, at the heart of the architecture design framework, I propose two optimization-based algorithms to tackle the exponential complexity of exact reliability computation, and enable scalable co-design of large, safety-critical systems for cost and fault tolerance.
I demonstrate, for the first time, the effectiveness of a contract-based approach on a real-life example of industrial relevance, namely the design of aircraft electric power distribution systems. I show that optimized selection of large, industrial-scale power system architectures can be performed in a few minutes, while design verification of controllers based on linear temporal logic contracts can achieve up to two orders of magnitude improvement in execution time with respect to conventional techniques. Finally, I conclude by presenting future research directions towards a full-fledged compositional framework for system design.

Biography: Pierluigi Nuzzo is a Ph.D. candidate in Electrical Engineering and Computer Sciences at University of California at Berkeley. He received the Laurea degree in Electrical Engineering (summa cum laude) from the University of Pisa and the Sant'Anna School of Advanced Studies, Pisa, Italy. His research interests include: methodologies and tools for cyber-physical system and mixed-signal system design; contracts, interfaces and compositional methods for embedded system design; energy-efficient analog and mixed-signal circuit design. Before joining U.C. Berkeley, he held research positions at the University of Pisa and IMEC, Leuven, Belgium, working on the design of energy-efficient A/D converters, frequency synthesizers for reconfigurable radio, and design methodologies for mixed-signal integrated circuits.
Pierluigi received First Place in the operational category and Best Overall Submission in the 2006 DAC/ISSCC Design Competition, a Marie Curie Fellowship from the European Union in 2006, the University of California at Berkeley EECS departmental fellowship in 2008, the U.C. Berkeley Outstanding Graduate Student Instructor Award in 2013, and the IBM Ph.D. Fellowship in 2012 and 2014.

Host: Prof. Massoud Pedram

Location: Hughes Aircraft Electrical Engineering Center (EEB) - 248

Audiences: Everyone Is Invited

Contact: Annie Yu