Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

Environment-driven reachability for timed systems

Ciprian Teodorov 1, 2 Philippe Dhaussy 1, 2 Luka Le Roux 1, 2
1 Lab-STICC_ENSTAB_ CACS_MOCS
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
2 Pôle STIC_IDM
ENSTA Bretagne - École Nationale Supérieure de Techniques Avancées Bretagne
Abstract : With an ever increasing complexity, the verification of critical embedded systems is a challenging and expensive task. Among the available formal methods, model checking offers a high level of automation and would thus lower the cost of this process. But, the scalability of this technique is hindered by the state-space explosion problem, which fuelled the research community since its inception. To address this challenge, in the case of real size systems, the theoretical, the methodological and the algorithmic axes have to be integrated. The context-aware verification (CaV) strives to do this by focusing on the identification, the isolation and the reification of the environment surrounding the studied system. It enables the use of specific algorithms with a major, positive, impact on the scalability of model checking. In this paper, we apply this technique to study a Landing Gear System (LGS) in the presence of failures. The problem has been decomposed in 885 independent verification units (called contexts). The analysis of 163 of these contexts on a 64 GB computer unraveled a 20 TB state space with more than 2.2 billion states. Moreover, using this approach arbitrarily long scenarios have been analysed using less than 10 GB of memory.
Type de document :
Article dans une revue
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-01373335
Contributeur : Annick Billon-Coat <>
Soumis le : mercredi 28 septembre 2016 - 15:25:41
Dernière modification le : mercredi 24 juin 2020 - 16:19:51

Identifiants

Citation

Ciprian Teodorov, Philippe Dhaussy, Luka Le Roux. Environment-driven reachability for timed systems. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2017, 19 (2), pp.229-245. ⟨10.1007/s10009-015-0401-2⟩. ⟨hal-01373335⟩

Partager

Métriques

Consultations de la notice

359