Discussion:Vérification de modèles

Anglicisme

Dommage de donner un titre en anglais à ce concept. Ne sommes-nous pas dans la partie française de l'encyclopédie? Le terme énumération de modèle aurait été beaucoup plus adéquat.

Pierre de Lyon 7 décembre 2005 à 20:16 (CET)

1) ce terme est celui utilisé depuis des années, et le changer pour une encyclopédie de ferait que brouiller les pistes 2) le model-checking consiste à vérifier automatiquement un modèle d'une spécification ou d'un programme, à l'aide d'un algorithme ; ce n'est pas une énumération de modèle (et il n'y a pas obligatoirement d'énumération exhaustive, heureusement !)

ATTENTION !! la technique de model-checking proposée dans cet article est l'algorithme de model-checking généralement utilisé pour la logique LTL, et c'est très loin d'être un cas général !

Cet argument d'autorité ne me convainc toujours pas dix ans après. même si depuis il y a un prix Turing! --Pierre de Lyon (discuter) 10 décembre 2015 à 15:21 (CET)

Je constate que la leçon au collège de France de Gérard Berry s'intitule La vérification de modèles (model-checking), il ya donc une piste. --Pierre de Lyon (discuter) 10 décembre 2015 à 15:29 (CET)

Le terme "vérification de modèles" est assez bon. Malheureusement, tout le monde utilise "model checking". --Fschwarzentruber (discuter) 1 avril 2016 à 19:32 (CEST)

Vulgarisation

Serait-il possible de vulgariser l'article par un exemple. De ce que je comprends du Model checking, je pense que ce serait assez simple et très explicite. Mes connaissances dans le domaine ne me permette malheureusement pas de proposer un exemple en étant sûr de ne pas faire d'erreurs. Perrinfa (d) 14 septembre 2009 à 16:53 (CEST)

Six ans après cette remarque je trouve l'article toujours aussi indigeste, bien que j'ai essayé de l'améliorer localement, mais je ne suis pas un spécialiste. --Pierre de Lyon (discuter) 10 décembre 2015 à 15:23 (CET)

J'ai réécrit et réorganisé l'article. J'ai commencé à ajouter des exemples. J'ai comme projet de rajouter un exemple sur un ascenseur. Je dois y réfléchir encore. --Fschwarzentruber (discuter) 1 avril 2016 à 19:33 (CEST)

Outils ?

La section "outils" me semble TI, et difficilement sourçable. Peut-être qu'il faudrait supprimer. --Roll-Morton (discuter) 1 avril 2016 à 14:32 (CEST)

Qu'est ce que TI veut dire ? On peut sourcer certains outils (par exemple des "system descriptions" dans certaines conférences). Bonne journée.

--Fschwarzentruber (discuter) 1 avril 2016 à 16:14 (CEST)

Pardon du jargon, ça veut dire « travail inédit » . La liste sous-entend que ces logiciels sont les plus importants, ce qui doit être sourcé. (Sinon chacun vient rajouter son logiciel maison, avec lien vers github). --Roll-Morton (discuter) 4 avril 2016 à 17:02 (CEST)

Bonjour, je suis d'accord avec toi. En plus, cette liste n'est pas informative. La page https://en.wikipedia.org/wiki/List_of_model_checking_tools est mieux faite car au moins elle propose un tableau. Après, on s'y perd aussi. Je ne connais pas assez les outils pour vraiment bien contribuer ici. Je ne sais pas encore quoi faire. --Fschwarzentruber (discuter) 5 avril 2016 à 09:32 (CEST)

Ça ne presse pas, on peut attendre de trouver des sources. --Roll-Morton (discuter) 5 avril 2016 à 09:35 (CEST)