Constructive Finite Trace Analysis with Linear Temporal Logic

We consider linear temporal logic (LTL) for run-time testing over limited time periods. The technical challenge is to check if the finite trace produced by the system under test matches the LTL property. We present a constructive solution to this problem. Our finite trace LTL matching algorithm yields a proof explaining why a match exists. We apply our constructive LTL matching method to check if LTL properties are sufficiently covered by traces resulting from tests.

The paper appeared in TAP'12. Here's a link to the paper and the talk.

The system has been implemented in Haskell and is applied in some real-world projects. Some of the Haskell source code will be made publicly available (later in the year).