An industrial application of formal model based development: the Metro Rio ATP case