Verifying HyperLTL properties in Event-B

Jean-Paul Bodeveix (1) , Thomas Carle (2) , Elie Fares (1) , Mamoun Filali (1) , Thai Son Hoang (3)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 IRIT-TRACES - Groupe de Recherche en Architecture et Compilation pour les systèmes embarqués
3 University of Southampton

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.

Domaines: Architectures Matérielles [cs.AR]; Systèmes embarqués

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⟩