Skip directly to: content | search

ExCAPE: Expeditions in Computer Augmented Program Engineering

Library-Based Scalable Refinement Checking for Contract-Based Design

PIs: Sangiovanni-Vincentelli (Berkeley), Tripakis (Berkeley)

Synthesis from Linear Temporal Logic is one of the most promising and successful example of correct-by-construction control software synthesis using formal methods. However the utilization of LTL synthesis to solve larger scale problems is still not feasible because of its time and space complexity. Contract-based design provides a theoretical framework that enables the application of platform based design principles, such as composability and reusability, also in the field of LTL synthesis. Sangiovanni-Vincentelli and Tripakis groups, are developing a framework to synthesize control software using contract-based design. A first result [INTSV14] has been the development of a technique to verify properties on system designs. Here each design is realized by composition of contracts, chosen from a pre-characterized library (with a particular emphasis on LTL Assume-Guarantee contracts). Thanks to concepts strongly inherent to contract theory, such as composition and refinement, together with the structured nature of the pre-characterized library, it is possible to reduce the problem size by iteratively finding abstractions of the initial design. With this method, it has been possible to observe a performance improvement in terms of execution time up to two orders of magnitude. This solution is being used in a number of case studies, including cyber-physical system design, where a design is defined composing library elements, and motion planning for robotic applications, where the library-oriented approach allows sharing the same high level contracts among different platforms. In this last scenario, the compositional nature of contracts allows dealing with complex tasks, where each contract describes a particular task. Contracts are then implemented by pre-synthesized controllers, loaded by the robot when needed.



Papers:

ExCAPE: Expeditions in Computer Augmented Program Engineering NSF National Science Foundation Award CCF-1138996