Stochastic validation of ATM procedures by abstraction algorithms