TCAS software verification using constraint programming

Arnaud Gotlieb; Arnaud Gotlieb

doi:10.1017/S0269888912000252

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.

Other Articles By Authors

TCAS software verification using constraint programming

INRIA – Rennes – Bretagne Atlantique

Certus Software V&V Centre

Corresponding author: Arnaud Gotlieb

Published online: 26 July 2012

Abstract: 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.

HTML

Acknowledgments

I am very grateful to Tristan Denmat who investigated the role of Abstract Interpretation in the ideas presented here. In particular, he provided us with the weak-join idea that comes from this community. Many thanks to David Delmas from Airbus Industries and the anonymous referees for their careful reading of the preliminary versions of the paper.

IEEE Spectrum (www.spectrum.ieee.org/nov04/4015).

Future generations of TCAS may propose three-dimensional escape maneuvers.

The standard classifies systems with 5 criticality levels: from the highest critical level A to the least critical E.

The implementation under test considers only a single threat, hence condition of line 11–12 cannot be satisfied.

TCAS is a real-time system that executes its loop-free software at each cycle.

In C, any non-null integer value is understood as true.

SICStus Prolog version 3.12.8.

www.irisa.fr/lande/gotlieb/resources.html

Rights and permissions

References (36)

About this article

Cite this article

Arnaud Gotlieb. 2012. TCAS software verification using constraint programming. The Knowledge Engineering Review 27(3)343−360, doi: 10.1017/S0269888912000252

Arnaud Gotlieb. 2012. TCAS software verification using constraint programming. The Knowledge Engineering Review 27(3)343−360, doi: 10.1017/S0269888912000252

{{lists.name}}

TCAS software verification using constraint programming

Abstract

Rights and permissions

References

About this article

Cite this article

Article Metrics

Access History

Other Articles By Authors