An industrial application of formal model based development: the Metrô Rio ATP case. - Alessio Ferrari 001; Mario Papini; Alessandro Fantechi; Daniele Grasso (SERENE, 2010)