The realization of complex cyber-physical systems is creating design and verification challenges that will soon become insurmountable with today’s engineering practices. While model-based design tools are already facilitating several design tasks, harnessing the complexity of the Internet-of-Things scenario is only deemed possible within a unifying methodology. This methodology should help interconnect different tools, possibly operating on different system representations, to enable scalable design space exploration and early detection of requirement inconsistencies.
In this talk, we show how a contract-based approach provides a formal foundation for a compositional and hierarchical methodology for cyber-physical system design, which can address the above challenges, and encompass both horizontal and vertical integration steps. We use assume-guarantee contracts and their algebra (e.g., composition, conjunction, refinement) to support the entire design process and enable concurrent development of system architectures and control algorithms. 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. Top-level system requirements are represented as contracts, by leveraging a set of formal languages, including mixed integer-linear constraints and temporal logic. Contracts are then refined by combining synthesis and optimization-based methods. We propose a set of optimization-based algorithms for efficient selection of cost-effective architectures under safety, reliability, and performance constraints over a large, mixed discrete-continuous design space. We demonstrate the effectiveness of our approach on industrial design examples, including aircraft electric power distribution and environmental control systems, showing, for instance, that optimal selection of industrial-scale power system architectures can be performed in a few minutes. Finally, we conclude by presenting future research directions towards a full-fledged compositional framework for system design.
Pierluigi Nuzzo is a Postdoctoral Scholar at the Department of Electrical Engineering and Computer Sciences of the University of California, Berkeley. He received the Ph.D. in Electrical Engineering and Computer Sciences from the University of California at Berkeley in 2015. He also holds the Laurea (M.Sc.) degree in Electrical Engineering (summa cum laude) from the University of Pisa and the Sant Anna School of Advanced Studies, Pisa, Italy. Before joining U.C. Berkeley, he was a Researcher at IMEC, Leuven, Belgium, and the University of Pisa, working on the design of energy-efficient A/D converters, frequency synthesizers for reconfigurable radio, and design methodologies for mixed-signal integrated circuits. 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. 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.