Title :
Proven correct monitors from PSL specifications
Author :
Morin-Allory, Katell ; Borrione, Dominique
Author_Institution :
Tima Lab., Grenoble
Abstract :
We developed an original method to synthesize monitors from declarative specifications written in the PSL standard. Monitors observe sequences of values on their input signals, and check their conformance to a specified temporal expression. Our method implements both the weak and strong versions of PSL FL operators, and has been proven correct using the PVS theorem proven This paper discusses the salient aspects of the proof of our prototype implementation for on-line design verification
Keywords :
hardware description languages; integrated circuit design; logic design; system-on-chip; theorem proving; PSL FL operators; PSL specifications; PSL standard; PVS theorem proven; declarative specification monitor; design verification; Automata; Circuit testing; Design engineering; Integrated circuit interconnections; LAN interconnection; Laboratories; Prototypes; Signal synthesis; Standards development; Very large scale integration;
Conference_Titel :
Design, Automation and Test in Europe, 2006. DATE '06. Proceedings
Conference_Location :
Munich
Print_ISBN :
3-9810801-1-4
DOI :
10.1109/DATE.2006.244079
