TCAS software verification using constraint programming. 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 5 articles )

Showing results 1 to 5 of 5.
Sorted by year (citations)

  1. Amadini, Roberto; Andrlon, Mak; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: Constraint programming for dynamic symbolic execution of JavaScript (2019)
  2. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  3. Hui, Zhanwei; Huang, Song; Ren, Zhengping; Yao, Yi: Metamorphic testing integer overflow faults of mission critical program: a case study (2013) ioport
  4. Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René: SAT solving for termination proofs with recursive path orders and dependency pairs (2012)
  5. Lazaar, Nadjib; Gotlieb, Arnaud; Lebbah, Yahia: A CP framework for testing CP (2012) ioport