HOME       UP       PREV       NEXT (Property Specification Language (PSL))  

Assertion forms: State/Path, Concrete/Symbolic.

Many assertions are over concrete state. For instance `Never is light A off when light B is on' .

Other assertions need to refer to symbolic values. For instance `The value in register X is always less than the value in register Y' .

State properties describe the current state only. For instance `Light A is off and light B is on'.

Path properties relate successive state properties to each other. For instance `light A always goes off before light B comes on '.

We shall see PSL requires the symbolic values be embedded in the bottommost `modelling layer' and that its temporal layer cannot deal with symbolic values. For instance, we cannot write `{ A(x);B(y) } |=> { C(x,y) }'.

(Note: the internal representation used by a checker tool for a concrete property can commonly use a symbolic encoding, such as a BDD, to handle an exponentially-large state space using reasonable memory, but that is another matter.)

The DUT is the device under test.

Blackbox testing is where tests are phrased only in terms of the externally visible behaviour of DUT.

Whitebox testing enables assertions to range over internal variables of the DUT.

8: (C) 2008-13, DJ Greaves, University of Cambridge, Computer Laboratory.