The aim of our work is to provide a quantified means of helping in the defi
nition of a new architecture for CAUTRA, a subset of the French Air Traffic
Control system. In this paper, we define a set of alternative architecture
s, give some elements for constructing their dependability models, and comp
are their availability. Modeling is carried out following a modular and sys
tematic approach, based on the derivation of block models at a high level o
f abstraction. In a second step, the blocks are replaced by their equivalen
t Generalized Stochastic Petri Nets to build up the detailed model of the a
rchitecture. The evaluations performed permit identification of a subset of
architectures whose availability meets the dependability requirements-and
also identification of the best architecture among this subset.