Verifying HyperLTL properties in Event-B - Fiabilité des Systèmes et des Logiciels
Conference Papers Year : 2024

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.
Fichier principal
Vignette du fichier
HYPER_LTL_ABZ.pdf (458.17 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-04662665 , version 1 (26-07-2024)

Identifiers

Cite

Jean-Paul Bodeveix, Thomas Carle, Elie Fares, Mamoun Filali, Thai Son Hoang. Verifying HyperLTL properties in Event-B. 10th International Conference on Rigorous State-Based Methods (ABZ 2024), Jun 2024, Bergame, Italy. pp.255-261, ⟨10.1007/978-3-031-63790-2_20⟩. ⟨hal-04662665⟩
243 View
18 Download

Altmetric

Share

More