"Model checking", un terme qui sort dans la presse

depuis l'annonce du premier prix Turing français
Amusant !

Je connais des ... qui, quand il a été question de définir les nouveaux programmes d'enseignement d'informatique, pour les fameuses habilitations de diplômes (DPLG, SGDG) adressées au Ministère, ont décidé qu'enseigner la spécification formelle des logiciels, la preuve, le model-checking c'était se couler : on n'allait pas attirer les clients, i.e. des étudiants. D'ailleurs à quoi bon aussi enseigner ce qu'est la machine de Turing ? (remarque d'un bac + 4 en informatique : je n'ai jamais vu cette marque de PC. Et ce n'était pas de l'humour), etc.
Alors, quand France Info annonce un prix Turing français, combien d' informaciens savent de quoi on parle ? J'ai déjà parlé de cela dans ce bloc-notes.
Il y a une semaine j'ai demandé à des Bac + 4 en informatique, ils étaient une vingtaine. Aucun ne savait.

Alors qu'est-ce que le "model checking" ! bof ! J'ai même eu un étudiant de Dess qui m'a dit "j'ai rencontré un chef de projet en informatique, il m'a dit qu'il ne savait pas ce qu'est un invariant, une précondition, un automate, alors on se demande bien pourquoi vous persistez à nous enseigner et nous demander d'utiliser ça."

Un lecteur m'a demandé de lui donner un petit exemple. Je lui propose d'installer le logiciel LTSA de Magee et Kramer
http://www.doc.ic.ac.uk/ltsa/
et d'étudier les exemples fournis
http://www.doc.ic.ac.uk/~jnm/book/