Dissertation Talk: A Platform-Based Approach to Verification and Synthesis of Linear Temporal Logic Specifications

Seminar: Dissertation Talk: EE | December 11 | 10-11 a.m. | Cory Hall, Cory 531 (Wang Room)

 Antonio Iannopollo, EECS

 Electrical Engineering and Computer Sciences (EECS)

The design of cyber-physical systems (CPS), which involve a coordination effort between several domains (i.e., software, real-time, physical, etc.), is a challenging task. To achieve design goals faster while guaranteeing system safety, the correct reuse of existing subsystems is essential. Formal specifications, such as those expressed in Linear Temporal Logic (LTL), have the potential to drastically reduce design and implementation efforts by enabling rigorous requirement analysis and ensuring the correct composition of reusable designs. Composing (formal) specifications, however, is a tedious and error-prone activity, and the scalability of existing formal analysis techniques is still an issue.

In this talk, we present a framework that leverages compositional design principles to enable correct-by-construction, platform-based synthesis of LTL specifications.
In our framework, a design is a composition of several components (which could be both hardware and software elements) described through their specifications, expressed as LTL assume/guarantee interfaces, or contracts.
One the one hand, we discuss how to efficiently synthesize compositions of contracts which satisfy a certain specification, presenting a technique based on counter-example guided inductive synthesis.
On the other hand, we describe how it is possible to decompose the synthesis task into several independent smaller problems, with the guarantee that composing the individual solutions will still satisfy the original specification.

 antonio@berkeley.edu