Item

Abstract

Virtually all verification and synthesis techniques assume that the formal
specifications are readily available, functionally correct, and fully match the
engineer's understanding of the given system. However, this assumption is often
unrealistic in practice: formalizing system requirements is notoriously
difficult, error-prone, and requires substantial training. To alleviate this
severe hurdle, we propose a fundamentally novel approach to writing formal
specifications, named specification sketching for Linear Temporal Logic (LTL).
The key idea is that an engineer can provide a partial LTL formula, called an
LTL sketch, where parts that are hard to formalize can be left out. Given a set
of examples describing system behaviors that the specification should or should
not allow, the task of a so-called sketching algorithm is then to complete a
given sketch such that the resulting LTL formula is consistent with the
examples. We show that deciding whether a sketch can be completed falls into
the complexity class NP and present two SAT-based sketching algorithms. We also
demonstrate that sketching is a practical approach to writing formal
specifications using a prototype implementation.