Model-Based Testing for Embedded Systems

624 Model-Based Testing for Embedded Systems

such as the IEEE standards SVA [10] and PSL [11] are typically used to formalize these

formulae. In this work, we focus on assertions expressed in PSL.

22.3.1 Temporal language—PSL

The Boolean layer of PSL enables building basic expressions commonly used by the other

layers. The core of the language is the Temporal layer, it provides the possibility to describe

complex temporal relations, evaluated over a set of evaluation cycles. In the following, we

consider formulae of the Foundation Language (FL) class of the Temporal layer, which

essentially represents linear temporal logic [22].

The semantics of PSL ...