Proven correct monitors from PSL specifications
The work
| Authors | Katell Morin-Allory; D. Borrione |
|---|---|
| Editors | |
| Type | misc |
| Year | 2006 |
| Citekey | morinallory2006proven |
Where it appeared
| Published in | Design, Automation, and Test in Europe |
|---|---|
| Pages | 1--6 |
Identifiers
| DOI | 10.1109/date.2006.244079 |
|---|---|
| OpenAlex | W2128354724 |
Access
| Landing page | https://doi.org/10.1109/date.2006.244079 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
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
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-26 13:52 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@misc{morinallory2006proven,
title = {Proven correct monitors from PSL specifications},
author = {Katell Morin-Allory and D. Borrione},
year = {2006},
journal = {Design, Automation, and Test in Europe},
pages = {1--6},
doi = {10.1109/date.2006.244079},
}
This record lives at https://refs.drheap.org/morinallory2006proven/ and will keep doing so.