Verifying HyperLTL properties in Event-B
Abstract
The study presented in this paper is motivated by the verification of properties related to hardware architectures, namely timing anomalies that qualify as counter-intuitive timing behaviour. They are avoided by a monotonicity property which is a Hyper-LTL property. We present how to prove some classes of Hyper-LTL properties with Event-B.
| Origin | Files produced by the author(s) |
|---|