On the Testability of Properties Patterns

Abstract

The specification pattern system (SPS) provides a simple methodology to specify program properties that can be used during software testing and verification. The testability concept establishes a connection between temporal properties and program traces to show which properties classes can actually be verified to reach a success/fail verdict. In this paper, we combine the SPS with the testability concept, showing that properties specified with certain patterns in global and local scopes are testable for programs with finite executions. This result implies that any property that is specified using this set of SPS patterns and scopes will receive a success/fail verdict when it is verified against a finite execution program by a model checker. In addition, we can analyze the program and property traces that are obtained in the verification process to extract data that can guide us in the test cases generation.

Appendices

Linear Temporal Logic (LTL)

The linear temporal logic (LTL) [1, 7] is largely used in formal verification theory to represent programs expected behavior through properties. Given a model $\sigma$ and temporal formulas $\varphi$ and $\gamma$, an inductive definition for the notion of a temporal formula $\varphi$ holding at a position $j \ge 0$ in $\sigma$, denoted by $(\sigma ,j)\vDash \varphi$ (satisfaction relation), is presented below.

Additional temporal operators can be defined as follows:

$$\begin{aligned} \boxed { \begin{array}{ll} \lozenge \varphi = True\; \mathcal {U}\; \varphi &{} \text {(Eventually operator)}\\ \square \varphi = \lnot \lozenge \lnot \varphi &{} \text {(Always/Henceforth operator)}\\ \varphi \;\mathcal {W}\; \gamma = \square \varphi \vee (\varphi \;\mathcal {U}\; \gamma ) &{} \text {(Weak Until operator)}\\ \end{array} } \end{aligned}$$

JPF - New Example

Here, consider the same scenarios and the same property of the example presented in Sect. 4:

$\square (Start \;\wedge \; \lnot Stop \rightarrow (\lnot Stop \;\mathcal {W}\; (Alarm \wedge \lnot Stop)))$

To achieve a success verdict with this property, we should include in the second scenario of the example a call to Alarm between Start and Stop. Then, JPF will proceed with the verification normally, and we could see a slight change in the automaton edges coverage since the paths that would be traversed in this case might be different from the previous example.

Comparing to the previous output (Listing 1.1), the coverage is 62.50 % since the edge (Node 0, Stop, Node 3) was not traversed due to the no occurrence of property violation. If a 100 % coverage was desirable, other scenarios and the generation of complementary test cases should be considered.