Résumé
Le premier cours du 2 avril 2013 a été double. La première heure a approfondi les notions générales présentées dans la leçon inaugurale, avec des exemples plus techniques. La deuxième heure a abordé l’étude des circuits combinatoires, en insistant sur leurs aspects temporels qui illustrent bien les différentes visions du temps.
Les formalisations du temps
Réaliser un système informatique, c’est prévoir ce qui peut se passer au cours du temps, le restreindre aux comportements souhaités, spécifier précisément et si possible formellement ces comportements, programmer pour que tout se passe comme spécifié, et vérifier la concordance de toutes ces actions. Les objectifs techniques sont de deux sortes, également difficiles : d’une part, spécifier, programmer et vérifier a priori la réalisation d’un système temporel et événementiel, et, d’autre part, analyser son exécution pour comprendre ses comportements dynamiques et être capable de trouver ses bugs.
Pour montrer que tout ne fonctionne pas toujours comme souhaité, j’ai présenté une collection de bugs liés au temps dans les systèmes embarqués grand public ou professionnels. Ils vont de problèmes idiots, comme l’absence de vérification d’une fonction temporelle apparemment non critique mais rendant l’objet inutilisable (lecteurs MP3 et jeux vidéo par exemple à cause des années bissextiles), à de plus subtils (erreurs cumulées d’arrondis dans la mesure du temps faisant échouer l’interception d’un missile Scud par un anti-missile Patriot lors de la guerre du Koweit, entraînant de nombreux morts).
J’ai ensuite analysé plus en profondeur les questions posées dans la leçon inaugurale, avec un leitmotiv : parler du temps, mais de manière formelle. J’ai expliqué par des exemples pourquoi les méthodes classiques sont insuffisantes.
