United Technologies Research Center
The design of large systems is divided into vertical refinement steps. The system is also partitioned into sub-systems that are designed in isolation and integrated in the prototyping and testing phase. Many design projects, commercial and military, incur in cost and schedule overruns mainly caused by errors discovered during testing. The correction of such errors typically requires undergoing long re-design cycles. The use of an appropriate methodology supported by tools can help avoiding these problems.
In this talk, we present a language for the contract-based specification of components and product families and we show how architectures can be checked for correctness. The language allows capturing static properties that are the ones typically considered in the preliminary design of systems. We then present methods to design and verify systems when dynamics and uncertainty are taken into account.
Given the expressiveness required to capture realistic systems, analysis methods do not scale suggesting synthesis approaches as promising techniques to refine a system through abstraction layers. It turns out that the selection of such abstraction layers is hard, mainly due to lack of abstract yet “meaningful” models.
Alessandro Pinto is a researcher in the Systems Department at the United Technologies Research Center (UTRC) Inc., Berkeley, California. His research interests are in the area of computer aided design for cyber-physical systems with particular emphasis on autonomous systems. He received a Ph.D. degree in Electrical Engineering and Computer Sciences from the University of California at Berkeley in 2008, and a M.S. degree in Electrical Engineering in 2003 from the same University. He holds a Laurea degree from the University of Rome “La Sapienza”. From 1999 to 2001, he was a consultant at Ericsson Lab Italy in Rome, Italy, working on the design of system-on-chips and wireless access networks.