Modeling the dependability of CAUTRA, a subset of the French air traffic control system

The aim of our work is to provide a quantified means helping in the definition of a new architecture for CAUTRA, a subset of the French Air Traffic Control system. To do this, we define alternative architectures for the CAUTRA whose availability is compared in order to select the architecture with the highest level of availability. Modeling is carried out following a modular and systematic approach, based on the derivation of black models at a high level of abstraction. In a second step, the blocks are replaced by their equivalent Generalized Stochastic Petri Nets to build up the detailed model of the architecture. Emphasis is placed on modeling interactions between hardware and software components