Being correct is not enough: efficient verification using robust linear temporal logic

While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this paper we present and study the logic rLTL which provides a means to formally reason about both correctness and robustness in system design. Furthermore, we identify a large fragment of rLTL for which the verification problem can be efficiently solved, i.e., verification can be done by using an automaton, recognizing the behaviors described by the rLTL formula varphi, of size at most O left( 3 |varphi| right), where |varphi| is the length of varphi. This result improves upon the previously known bound of Oleft(5|varphi| right) for rLTL verification and is closer to the LTL bound of Oleft( 2|varphi| right). The usefulness of this fragment is demonstrated by a number of case studies showing its practical significance in terms of expressiveness, the ability to describe robustness, and the fine-grained information that rLTL brings to the process of system verification. Moreover, these advantages come at a low computational overhead with respect to LTL verification.