Princeton University

School of Engineering & Applied Science

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

Pierluigi Nuzzo
E-Quad, B205
Thursday, March 26, 2015 - 4:30pm

In cyber-physical systems (CPS), computation, communication and control are tightly combined with physical processes of different nature. Without a comprehensive modeling formalism and a rigorous, unifying design framework, CPS integration remains ad hoc. In this talk, we introduce a design methodology that addresses the complexity and heterogeneity of cyber-physical 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 our 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. To enable formal requirement analysis and early detection of inconsistencies, we represent the top-level system requirements as contracts, by leveraging a front-end pattern-based specification language and a set of back-end languages, including mixed integer-linear constraints and temporal logic. We show how key analysis tasks, such as refinement checking, can indeed be made more efficient when a system is described based on a precharacterized library of components and contracts. We then illustrate how top-level contracts can be refined to achieve independent implementation of system architecture and control algorithm, by combining synthesis from requirements, optimization and simulation-based design space exploration methods. At the heart of our architecture design framework, we propose two optimization-based algorithms to tackle the complexity of exact reliability computation, and enable scalable co-design of large, safety-critical systems for cost and fault tolerance. We 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 (EPS). In our framework, optimal selection of large, industrial-scale EPS architectures can be performed in a few minutes, while design validation of EPS controllers based on linear temporal logic contracts shows up to two orders of magnitude improvement in terms of execution time with respect to conventional techniques.
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.