TCAS software verification using Constraint Programming

Abstract : Safety-critical software must be thoroughly verified before being exploited in commercial applications. In particular, any TCAS (Traffic Alert and Collision Avoidance System) implementation must be verified against safety properties extracted from the anti-collision theory that regulates the controlled airspace. This verification step is currently realized with manual code reviews and testing. In our work, we explore the capabilities of Constraint Programming for automated software verification and testing. We built a dedicated constraint solving procedure that combines constraint propagation with linear programming to solve conditional disjunctive constraint systems over bounded integers extracted from computer programs and safety properties. An experience we made on verifying a publicly available TCAS component implementation against a set of safety-critical properties showed that this approach is viable and efficient.
Type de document :
Article dans une revue
Knowledge Engineering Review, Cambridge University Press (CUP), 2012, 27 (3), pp.343--360
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00807905
Contributeur : Arnaud Gotlieb <>
Soumis le : jeudi 4 avril 2013 - 15:25:27
Dernière modification le : jeudi 4 avril 2013 - 16:35:05
Document(s) archivé(s) le : vendredi 5 juillet 2013 - 04:18:43

Fichier

CT4ATCgotlieb.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00807905, version 1

Citation

A. Gotlieb. TCAS software verification using Constraint Programming. Knowledge Engineering Review, Cambridge University Press (CUP), 2012, 27 (3), pp.343--360. 〈hal-00807905〉

Partager

Métriques

Consultations de la notice

125

Téléchargements de fichiers

484