Model-Checker-Based Testing of LTL Specifications

Formal verification techniques for software typically start with formal specifications of software behavior. Several automated tools use linear temporal logic (LTL) to specify behavioral properties of software. A significant hurdle to the use of formal approaches is the development of formal specifications.This paper introduces the property testing tool (Protest), which automatically generates and tests formulas representing software specifications, in particular, specifications based on SPS and composite propositions. Protest takes an execution trace and builds a model of the trace. It then uses the NuSMV model checker to test whether the given formula is satisfied by the model. The output of the model checker is compared to the expected result to determine if the test case passes or fails.