Rien ne va de soi. Rien n'est donné. Tout est construit.

"les problèmes ne se posent pas d'eux-mêmes. C'est précisément ce sens du problème qui donne la marque du véritable esprit scientifique. Pour un esprit scientifique, toute connaissance est une réponse à une question. S'il n'y a pas eu de question, il ne peut y avoir connaissance scientifique. Rien ne va de soi. Rien n'est donné. Tout est construit."

Gaston Bachelard, La formation de l'esprit scientifique, Vrin, p. 1

Bref, y'a du boulot ! Le pré-cuit, le pré-maché, le digest c'est indigeste. Ca fait crever les sociétés... et les "promotions" d'étudiants.
Ma bonne dame, mon bon monsieur, notre promotion universitaire : trois années d'études pour le prix d'une ! Pas d'examens, pas de dossiers, pas de livres à lire, de cours à suivre, d'exercices à pratiquer. Et le wifi pour tous.


Madame la boulangère, du pain pas cuit s'il vous plait ! que de fois j'entends cette demande formulée par de jeunes clients ... Le femme du boulanger, elle en a de la chance ! bientôt elle ne sera plus réveillée en pleine nuit par son boulanger de mari. Merci client, merci client.

la première connaissance objective ... une première erreur

"Au spectacle des phénomènes les plus intéressants, les plus frappants, l'homme va naturellement avec tous ses désirs, avec toutes ses passions, avec toute son âme. On ne doit donc pas s'étonner que la première connaissance objective soit une première erreur."

Gaston Bachelard, La formation de l'esprit scientifique, Vrin, page 54

Le programme de la conférence FORMED 2008, Budapest

ICI

Votre déclaration d'amour pour la Saint-Valentin

Robert Solé dans son billet du Monde de ce jour, nous informe que la Cité des sciences et de l'industrie de Paris propose son assistance.Sur le site http://www.cite-sciences.fr/declaration-st-valentin/, vous indiquez le prénom de l'élu(e), sa qualité première, la couleur de ses yeux, son adresse électronique, et en moins d'une seconde la machine lui envoie un joli poème de votre part.Robert Solé a essayé ... lire son papier

Je vous offre un psychothérapeute

"Les enseignants doivent de nos jours être des personnes à l'écoute des problèmes des élèves"
a dit ....
alors, voici

ICI

Parlez-lui en Anglais.

Je vous adresserai ses honoraires. Paiement en euros, cartes acceptées : Visa, Master card, American Express

Mais si vous voulez une thérapie en français, c'est moins cher, mais donc bien moins efficace. Lisez Freud !

ICI

Les TD au labo d'automatisme

ICI

Du fait du comportement de la majorité d'étudiants d'il y a 3 ans, vous en avez de la chance !
ces td sont supprimés.

Economie : le département informatique n'a plus à participer au financement du labo et comme ses étudiants séchaient ces td, on a amélioré nos performances !

Ma poubelle n'était pas vidée

J'ai donc le cours de parallélisme (projet Européen Papillon).

Le parallélisme, un dictionnaire en ligne

ICI

et n'oubliez pas les pages du module SPEC2 (je me répète. D'aucuns disent que c'est de la bonne pédagogie. Je ne le pense pas !)

Autre chose : vous avez maintenant les sujets des "PT".
J'ai vu que mon sujet a été découpé en plusieurs sujets. Il faut considérer que mes questions font un tout cohérent. Cherchez le lien...

J'avais proposé (un courriel envoyé à tous) un cours complet sur le parallélisme. Pas de réponse, il est passé à la poubelle. Il avait été financé par des fonds européens. Bof, bof, bof...

Je vous rappelle que les photos des tableaux de cours et de TD de 2006-2007 sont sur ce bloc-notes

...je sais, il faut y naviguer un peu. Mais les voyages forment la jeunesse !

Cours du 11 février 8h15-9h15

Amphi 4

Le cours s'est déroulé par une belle matinée. Ciel tout bleu. Froid sec agréable à 8h 15. Amphi bien chauffé.

11 absents du groupe 1
19 absents du groupe 2
7 absents du groupe 3
18 absents du groupe 4



J'ai traité :

• J'ai distribué une petite spec en B. Il s'est agi de faire le diagramme de transition d'états. J'ai fait un automate simple et un automate structuré (un automate de Harel).
• La prochaine fois, je ferai la spec en B événementiel
• le renommage. Illustré par des chaussettes thaïlandaises et des gants français et par un exemple en FSP(LTSA) Client/Serveur
• le produit de processus (avec FSP)
• la sémantique du losange pour le parallèlisme. Illustrations avec exemples en FSP
• processus types et instances de processus types (processus) en FSP
• un exemple de partage de ressources

Ca c'était pour avoir l'essentiel de LTSA pour pouvoir l'utiliser pour les différents exercices de td

Je suis passé alors aux

• Réseaux de Petri, avec un exemple. J'ai fait l'automate (un état est un vecteur de marquage). J'ai bien insisté : avec les RDP, il ne s'agit pas de déplacement de jetons. Un marquage d'une place avec 2 jetons n'est ni plus ni moins que dire que cette place a pour valeur l'entier 2.
• Il n'y a pas forcément conservation du nombre de jetons. Il peut y avoir dans un problème donné, un invariant qui dit par exemple que le marquage de telle place + le marquage de telle autre doit toujours être égal à 5. Mais cela n'est pas une loi générale des RDP !

J'ai distribué un texte complément au cours de Michael Jackson et un texte sur le modèle relationnel avec la notation NIAM. Bien sûr, il y aura des questions du DS sur ces textes.

J'ai à la disposition des étudiants intéressés, un texte rédigé par J.F. Monin et J. Sifakis (Prix Turing) intitulé "Eléments de classification des méthodes formelles". On y retrouve notre programme de Spec1 et celui de Spec2.

Portail de la sécurité informatique

ici

Model-checking

Interview très courte de J. Sifakis sur le Model Checking. Pour ceux qui ont raté le cours ... et les TD !

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 "