Specification Mining: New Formalisms, Algorithms and Applications

Specification is the first and arguably the most important step for formal verification and correct-by-construction synthesis. These tasks require understanding precisely a design’s intended behavior, and thus are only effective if the specification is created right. However, it is extremely difficult to manually create a complete suite of good-quality formal specifications. Many real-world experiences indicate that poor or the lack of sufficient specifications can easily lead to misses of critical bugs.

This talk presents research that seeks to mitigate the manual and error-prone process of creating formal specifications through automation. The overarching theme is specification mining – the process of inferring likely specifications. We present a collection of novel formalisms and techniques that are tailored for a variety of different applications. We study two topics at large – verification and synthesis. In verification, we show that relevant and meaningful specifications can be mined dynamically from traces of a design, and are useful also for bug localization. In synthesis, we study the problem of synthesis from temporal logic specifications and focus on the problem of finding environment assumptions. We show that, by analyzing the counterstrategy of an unrealizable specification, we can systematically generate candidate environment assumptions that guide the specification towards realizability. In addition, this counterstrategy-guided synthesis approach enables the automatic construction of a new class of semi-autonomous controller, called human-in-the-loop controllers. Further, we highlight efforts on incorporating Natural Language Processing techniques to make this technology more accessible to non-expert users of formal methods.

We conclude the talk by reviewing our efforts on tackling the general problem of model construction and specification creation, and discussing their increasing relevance in the emerging world of cyber-physical systems.

发言人详细信息

Wenchao Li is a postdoctoral fellow in the Formal Methods and Dependable Systems group at SRI International. He recently received his M.S. and Ph.D in Electrical Engineering and Computer Sciences from UC Berkeley, where he was advised by Sanjit A. Seshia. His research primarily focuses on analyzing and improving the dependability of computing systems. He is the recipient of the 2013 Leon O. Chua Award for nonlinear science at UC Berkeley.

日期:
演讲者:
Wenchao Li
所属机构:
SRI International