Model checking à Carnegie Mellon

http://www.cs.cmu.edu/~modelcheck/

Joseph SIFAKIS, premier prix Turing français

Le français Joseph Sifakis vient d'obtenir
le prix Turing 2007. C'est le
premier français obtenant ce prix, considéré
comme "le Nobel de
l'informatique". Joseph Sifakis est un
spécialiste du "model checking".
Il y a deux approches de la vérification
des logiciels :
- la preuve que nous traitons dans le cadre
de notre enseignement de la méthode B dans
notre module Spec1  en première année d'IUT
- la "vérification de modèles" que nous traitons
dans le cadre de notre module Spec2 en première
année d'IUT.
(Mais nous NE traitons pas des algorithmes de
"model checking").
Parmi les techniques utilisées en "model checking"
il y a les BDD (ne pas confondre avec les Bases De
Données ou avec les Bases de Données Déductives !)
lire ici
http://www2.cnrs.fr/presse/communique/1280.htm
http://www.acm.org/press-room

Il a obtenu ce prix avec Avec Edmund Clarke
(Carnegie Mellon University, USA)
Allen Emerson (University of Texas, Austin, USA).

Ces deux universités américaines sont bien
connus pour leurs travaux en informatique et ont
déjà eu des Prix Turing.

Les pages web de Joseph Sifakis

Extrait d'une courte présentation de Joseph Sifakis
et Jean-François Monin dans Arago 20
Applications des techniques formelles au logiciel,
Observatoire Français des Techniques Avancées,
Lavoisier, ISBN 2-906028-06-1

"On peut distinguer deux approches principales à
la vérification :

• celle qui met en oeuvre un système d'inférence, i.e. un ensemble bien défini et formalisé de règles de raisonnement issues de la logique (modus ponens, récurrence, substitution de valeurs égales, etc.) ; les outils de support sont des assistants à la preuve (PVS, HOL, Coq, atelier B, LP,...)
• celle qui se fonde sur la construction d'un modèle généralement fini qui représente le système de transition représentant le comportement de l'application modélisée. La vérification des propriétés s'effectue en parcourant exhaustivement ce modèle. Les outils support sont basés sur le principe de l'évaluation des propriétés sur un modèle, connu sous le nom de model checking (MEC, Caesar-Aldebaran, Auto, Spin, Cospan, SMV, ...)

[...] concernant la seconde approche, des techniques de représentation implicite ou symbolique des états permettent de condenser la représentation du modèle. Notons, en particulier, la technique des BDD pour la représentation symbolique des fonctions booléennes, qui trouve des applications intéressantes à la vérification des systèmes à états finis."

Génie logiciel, nouvelles de l'industrie

Nouvelles de l'industrie :

http://www.siemens.com/index.jsp?sdc_p=pofc58l2smnu18

Siemens utilise la méthode B, comme vous tous !

Le cours du 4 février 2008

Comme annoncé (mais le nombre d'étudiants qui est allé sur ce blog pour préparer le cours ne dépasse pas le nombre de doigts d'une main !), il y a eu l'exposé de Michaël Jackson.

Les nouvelles technologies qu'ils disent ! ya ka faire de li teaching pour remonter le niveau ... des profits des marchands d'ordinateur !

• pourquoi ne pas commencer par décrire les entrées et sorties des opérations (en B on dirait les signatures)
• pourquoi un schéma conceptuel de données est généralement illisible (langue de bois) si l'on n'a pas défini les événements du système et leur ordonnancement
• il n'y a des objets que parce qu'il y a du parallèlisme
• exemple de la bibliothèque
• le livre id345 est-il à la bibliothèque ? non sens de la question si on n'a pas défini quel sens a "est à". Je vous renvoie à mon cours sur les 4 sens du verbe être et sur la structure de la phrase d'Aristote (Objet copule attribut)
• la communication par flot de données et par vecteur d'états (asynchrone)

J'ai terminé l'exposé sur l'encapsulation vs l'ensemble des vecteurs d'état des processus mis en variables globales.

L'exposé est sur publicinfo, dossier dvd, sous-dossier video-ts, sous-sous dossier VTS-01

Prochain cours portera sur :

- qu'est-ce qu'un état ?

- parallèlisme

- communication entre processus

- deadlock, livelock, progression

Michaël Jackson, à Nantes, lundi 4 février 2008

à 8h 15, Amphi 4, 3 rue Ml Joffre

Pour en savoir plus :

* Michael A. Jackson

http://en.wikipedia.org/wiki/Michael_A._Jackson
http://mcs.open.ac.uk/mj665/

et
http://www.iut-nantes.univ-nantes.fr/~habrias/spec2/jsd.html

Attention, se méfier de la "non univocité des noms" !

Michaël Jackson, à Nantes, lundi 4 février 2008

à 8h 15, Amphi 4, 3 rue Ml Joffre

Pour en savoir plus :

   * Michael A. Jackson

http://en.wikipedia.org/wiki/Michael_A._Jackson
http://mcs.open.ac.uk/mj665/

et
http://www.iut-nantes.univ-nantes.fr/~habrias/spec2/jsd.html

Attention, se méfier de la "non univocité des noms" !

L'informatique ?

Je viens de retrouver un extrait d'un livre, dont j'ai perdu la référence.

Voici le titre du chapitre 3

"A test for practitioners of the science/art/craft/trade/racket of software design and development"

et ces deux citations :

"Ignorance, when voluntary, is criminal, and a man may be properly charged with that evil which he neglected or refused to learn how to prevent."
Samuel Johnson (1709-1784)

"Pure mathematices do remedy and cure many defects in the wit and faculties of individuals; for if the wit be dull, they sharpen it; if too wandering, they fix it; if too inherent in the sense, they abstract it."
Francis Bacon (1561-1626)

Je tiens à votre disposition le test.

A étudier avant le prochain TD

Allez à
http://informatiqueetorganisationsociale.blogspot.com

pour être prêts à répondre à la question que je poserai lors du projet TD.
Lire ce qui concerne "l'affaire de la Société Générale"
et lire dans http://nantespec1.blogspot.com
ce qui concerne Nabuco et Sifiac

Exercice. Faisons feu de tout bois

Je reçois ce courriel du directeur du labo d'informatique de Nantes.

A faire : l'automate (le diagramme de transition d'états) du processus. Vous étiquetterez les transitions par les événements.

"Bonjour à tous,

Le CNRS et le précédent conseil du LINA viennent de donner leur accord pour la composition de notre nouveau conseil de laboratoire.Nous vous proposons donc d'organiser l'élection de ses membres élus selon l'agenda ci-dessous et les règles décrites dans un courriel (un peu long) à suivre.Ce conseil joue un rôle essentiel dans la vie du laboratoire dont il rythme les prises de décision importantes.Nous vous invitons donc à vous porter nombreux candidats.

Pierre Cointe et Béatrice Daille

PS.

Agenda
vendredi 8 février12h00 : date et heure limites de modification des listes
jeudi 14 février 18h00 : date et heures limites de déclaration des candidatures
lundi 3 mars 10h00 : date et heure de début de réception des bulletins de vote aux trois secrétariats du LINA
vendredi 7 mars 12h00 : date et heure de clôture de réception des bulletins de vote aux trois secrétariats du LINA "

Le cours du 28 janvier 2008

- J'ai récupéré les travaux à faire chez soi
- j'ai illustré ce qu'il y avait à faire en l'application à l'American Film Star de M. Jackson.
- je suis passé d'un automate de Moore à un automate de Mealy
- j'ai traité des automates cellulaires (le jeu de la vie de Conway)
- je suis passé d'arbres Jackson à des specs en FSP (atelier LTSA)
- j'ai introduit la communication entre processus
- le produit d'automates étiquetés
- vous pouvez installer LTSA sur vos machines persos (c'est gratuit)
- voir les messages sur ce bloc-notes (consultez ceux de l'an dernier)


Prochain cours :

- je continuerai sur FSP
- composition parallèle de processus séquentiels
- deadlock
- diagramme de transitions d'états d'une spec FSP

Le cours est disponible sur la Toile (lire ce bloc-notes)