< retour aux publications

A proof of correctness for the construction of property monitors

Auteur(s) : K. Morin-Allory, D. Borrione

Doc. Source: Tenth IEEE International High-Level Design Validation and Test Workshop (HLDVT'05)

Pages : 237-244

Doi : 10.1109/HLDVT.2005.1568843

We prove the correctness of an original method for generating components that capture the occurrence of events, and monitor logical and temporal properties of hardware/software embedded systems. The properties are written in PSL, under the form of assertions in declarative form. The method is based on a library of primitive digital components for the PSL temporal operators. These building blocks are interconnected to construct complex properties, resulting in a synthesizable digital module that can be properly linked to the digital system under scrutiny. The proof reported in this paper applies to the weak version of all “foundation language” operators.