Résumé
Kim Larsen est un des acteurs principaux de la vérification formelle de systèmes temps-réel, à travers le centre CISS () qu’il a cofondé à Aalborg (Danemark). Il est l’architecte du système de vérification UPPAAL (pour Uppsala/Aalborg), qui est le système de vérification d’automates temporisés le plus puissant et le plus utilisé actuellement. Après un rappel sur les systèmes embarqués et la vérification formelle qualitative et quantitative, des propriétés logiques et temporelles des systèmes, il présente le design d’UPPAAL et ses principales fonctionnalités à travers l’exemple d’un système de signalisation ferroviaire, puis les principaux algorithmes à l’œuvre. Il illustre ensuite la puissance de la vérification temporisée par plusieurs exemples industriels : détection et correction d’un très ancien bug qui n’avait jamais pu être caractérisé auparavant dans les systèmes audio/vidéo Bang & Olufsen, vérification de protocoles chez Philips, applications diverses dans l’automobile, ordonnancement de tâches temporisées, etc.
