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).
Monday, 4 June 2012
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.