Un chateau pas très fort : percez les mécanismes des systèmes informatiques les plus complexes !

Cette activité illustre une méthode de vérification formelle de systèmes informatiques appelée model-checking (et donc littéralement vérification de modèles). Le principe est de représenter son système (ici le château) par un modèle (ici un automate), qui a l'avantage d'avoir une définition très précise. En clair quand on regarde l'automate du château on sait précisément tous les passages qui existent entre deux pièces. De même on va représenter les propriétés qui nous intéressent de manière formelle, dans un langage logique. Avec cette activité, tout en jouant dans un château fort, on entre vraiment dans les mécanismes de vérification formelle de systèmes informatiques. On apprend à écrire une formule logique pour décrire précisément une propriété, puis on voit comment l'ordinateur vérifie si un système la satisfait. Et on utilise au passage les opérateurs logiques classiques. Basée sur le concept des activités débranchées proposées aux plus jeunes, cette activité permet de s'initier au model-checking de manière manuelle.