A C-language binding for PSL

Short Description
cation 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 …

Website: research.microsoft.com | Filesize: 153kb

Content
A C-language binding for PSL
Ping Hang Cheung, Alessandro Forin
Microsoft Research
September 2006
Technical Report
MSR-TR-2006-131
Microsoft Research
Microsoft Corporation
One Microsoft Way
Redmond, WA 98052- 2 -
A C-language binding for PSL
Ping Hang Cheung, Alessandro Forin
Microsoft Research, One Microsoft Way, Redmond, WA, USA
cheung@cecs.pdx.edu, sandrof@microsoft.com
Abstract. 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.
Keywords: Property Specification Language, C, Assertion Based Verification
1. Introduction
Assertions Based Verification (ABV) is an approach that is used by hardware design…