yAro :
Bon pr etre précis ... météor a été analysé avec la méthode SADT puis écrit en langage B (c pas de la prog c des preuves)

Pour etre plus précis, c'est de "l'event B", une variante du B avec une gestion poussée de tout ce qui est évenement (toujours inventée par Jean-Raymond Abrial d'ailleurs ) C'est plus propre que par exemple une approche du type CSP2B ou CSP//B