A C-language binding for PSL

In recent years we have seen an increase in the complexity of embedded system design and in the difficulties of their verification. As a result, engineers have been trying to verify the specifications at a higher level of abstraction. In this paper we present an automated tool which is able to perform runtime verification of a program’s logical properties asserted by the programmer. The idea is to leverage the Assertion Based Verification language PSL, which is widely used by hardware engineers, extending it to the software verification of C language programs. The properties expressed in a simple subset of PSL are evaluated by the tool during full-system simulation. Like in hardware Assertion Based Verification, the tool can handle both safety properties (absence of bad events) and liveness properties (good events eventually happen). The liveness property is not widely supported in existing verification tools.