Discussion utilisateur:Simo.93/Brouillon

Première lecture du 03/01/2017 pour la forme - Abdessamad J.

Bonjour, je suis Abdessamad JARIR, voici quelques points que j'ai pu noter à propos de votre articles premièrement je commence par la forme :

Bonjour Abdessamad J, je suis Lahcene A je suis l'un des rédacteurs de cet article.Je vous remercie pour ces remarques aux quelles j'essayerai de répondre. Cordialement --LahceneTiir (discuter) 6 janvier 2017 à 14:26 (CET)

dans le résumé introductif j'aurai bien aimé avoir des liens wiki pour la définition des termes suivants : SPIN, ComFoRT.--Abdessamad J (discuter) 3 janvier 2017 à 11:12 (CET)

le lien de Spin est fait --LahceneTiir (discuter) 6 janvier 2017 à 14:19 (CET)

par contre il n'ya pas de lien pour ComFoRT --LahceneTiir (discuter) 6 janvier 2017 à 14:19 (CET)

généralité

définition

Système d'exploitation

Je pense qu'il faut pas laisser operating_system et la traduire en système d'exploitation.--Abdessamad J (discuter) 3 janvier 2017 à 11:16 (CET)

Ce paragraphe "Prouver formellement ...." et tout les autres paragraphes jusqu’à la section "Outils de vérifications" ne sont pas sourcées.--Abdessamad J (discuter) 3 janvier 2017 à 11:16 (CET)

Il faut changer OS en SE pour (Système d'exploitation).--Abdessamad J (discuter) 6 janvier 2017 à 14:14 (CET)

fait --LahceneTiir (discuter) 6 janvier 2017 à 14:39 (CET)

Il est inévitable d’avoir des erreurs dans du code informatique .. => il faut remplacer le "du" en "un", sinon il faut dire sur quel code informatique vous parlez.--Abdessamad J (discuter) 6 janvier 2017 à 14:14 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 14:39 (CET)

... par conséquent plus la taille du code est élevé ... => "e" oublié à la fin du élevé.--Abdessamad J (discuter) 6 janvier 2017 à 14:30 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 14:39 (CET)

Méthodes de vérifications

Model checking

Changer le titre Model checking en Vérification de modèles.--Abdessamad J (discuter) 6 janvier 2017 à 14:30 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 14:51 (CET)

Le model checking ne travail pas => "travailler" mal conjugué, changer en "ne travaille pas" --Abdessamad J (discuter) 6 janvier 2017 à 14:30 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 14:53 (CET)

une méthode qui pourra être efficasse ... => "efficasse" le mot mal écrit changer en "efficace".--Abdessamad J (discuter) 6 janvier 2017 à 14:30 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 14:55 (CET)

vu qu'il sont assez volumineux en taille ... => "s" oublié dans "il".--Abdessamad J (discuter) 6 janvier 2017 à 14:39 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 15:02 (CET)

cela prendrai énormément de temps ... => je pense qu'il faut conjuguer le verbe "prendre" au présent puisque vous parlez sur un fait réel (résulat d'une expérimentation).--Abdessamad J ([[Discussion

utilisateur:Mywiki16|discuter]]) 6 janvier 2017 à 14:50 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 15:02 (CET)

Le début de ce paragraphe "De plus ... jusqu’à "erreurs" est mal formé + faut utiliser "ce" au lieu de "se" dans "se qui est fait".--Abdessamad J (discuter) 6 janvier 2017 à 14:56 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 15:04 (CET)

• J'aurai aimé avoir un lien wiki vers SLAM!.

theorem proving

• Manque la deuxième '"' et "de" après le but.--Abdessamad J (discuter) 6 janvier 2017 à 15:02 (CET)
• ... on va en déduire une preuve mathématique et vérifier qu'elle confirme ces propirétés. => faut changer "elle" en "il" puisque vous parlez sur le noyau.Le mot "propirétés" mal écrit changer en "propriétés"--Abdessamad J (discuter) 6 janvier 2017 à 15:15 (CET)
• Manque le majuscule au début de cette phrase "la taille du ...".--Abdessamad J (discuter) 6 janvier 2017 à 15:21 (CET)
• ... cette méthode sur tout types d'OS ... => "s" à la fin de tout au lieu de "t".--Abdessamad J (discuter) 6 janvier 2017 à 15:21 (CET)
• ... en particulier les plus complex ... => manque "es" à la fin de "complex".--Abdessamad J (discuter) 6 janvier 2017 à 15:25 (CET)
• ... la vérification des preuvent mathématiques ... => "preuvent" avec "es" à la fin au lieu de "ent".--Abdessamad J (discuter) 6 janvier 2017 à 15:27 (CET)
• ... cette preuve soit compliqué ... => manque "e" à la fin de "compliqué".--Abdessamad J (discuter) 6 janvier 2017 à 15:29 (CET)
• Cette phrase "A noter que comparer au model checking...mais aussi pourquoi." => je trouve que c'est mal formée.--Abdessamad J (discuter) 6 janvier 2017 à 15:32 (CET)

fait--Narjis.taou (discuter) 8 janvier 2017 à 21:47 (CET)

---

Normalement, tout à été corrigé, merci--Loik D./Tiir IIR (discuter) 9 janvier 2017 à 11:31 (CET)

Preuve par le code

• ... la PCC créé ... => "créé" avec "e" à la fin au lieu de "é".--Abdessamad J (discuter) 6 janvier 2017 à 15:40 (CET)
• ... Ov va trouver deux types de PCC : => je pense vous voulez dire "on" au lieu "ov" :).--Abdessamad J (discuter) 6 janvier 2017 à 15:40 (CET)

fait--Narjis.taou (discuter) 8 janvier 2017 à 21:47 (CET)

Critères communs

• ... et cela a attisé l’intérêt des chercher ... => l’intérêt des chercheurs vous voulez dire ?--Abdessamad J (discuter) 6 janvier 2017 à 15:44 (CET)
• ... les critères communs sont considéré ... => manque de "s" à la fin de "considéré".--Abdessamad J (discuter) 6 janvier 2017 à 15:48 (CET)
• ... et adhère à un modèle de procès légal. => "adhère" avec "ent" à la fin.--Abdessamad J (discuter) 6 janvier 2017 à 15:48 (CET)
• La phrase "Les critères communs ... comme un standard pour la sécurité informatique" est déjà dite dans le paragraphe précédent.--Abdessamad J (discuter) 6 janvier 2017 à 15:53 (CET)

Effectivement, corrigé ;-)--Loik D./Tiir IIR (discuter) 9 janvier 2017 à 11:40 (CET)

• ... les standards précédent ... => "précédent" avec "s" à la fin.--Abdessamad J (discuter) 6 janvier 2017 à 15:57 (CET)
• Il vaut mieux avoir un lien vers ces standards ITSEC, TCSEC.--Abdessamad J (discuter) 6 janvier 2017 à 15:57 (CET)
• ... les CC sont plus orienté ... => "orienté" avec "s" à la fin.--Abdessamad J (discuter) 6 janvier 2017 à 16:05 (CET)
• ... les CC sont plus orienté produit et moins orienté procédures que les anciens standards. => "produit" sans "s" et procédures avec "s" ???, soient les deux sans "s" ou avec "s".--Abdessamad (discuter) 6 janvier 2017 à 16:05 (CET)
• ... ils représentent une forte avancé vers la sécurité ... "avancé" avec "s" à la fin.--Mywiki16 (discuter) 6 janvier 2017 à 16:15 (CET)
• ... mais surtout assure ... => "assure" avec "ent" à la fin.--Abdessamad J (discuter) 6 janvier 2017 à 16:15 (CET)
• ... En se qui concerne les noyaux ... => faut utiliser "ce" au lieu de "se".--Abdessamad J (discuter) 6 janvier 2017 à 16:15 (CET)
• ... le nombre de noyau ... le nombre de noyau => "noyau" avec x à la fin.--Abdessamad J (discuter) 6 janvier 2017 à 16:15 (CET)
• Manque des notes pour ITSEC, TCSEC.--Abdessamad J (discuter) 6 janvier 2017 à 17:07 (CET)

Pour se qui est des fautes d'orthographe, tout à normalement été corrigé.--Loik D./Tiir IIR (discuter) 9 janvier 2017 à 11:40 (CET)

Outils de vérifications

Langages formels

J'aurai aimé avoir un lien wiki vers Langage formel et Haskell. --Abdessamad J (discuter) 6 janvier 2017 à 16:32 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 17:14 (CET)

Il vaut mieux dire "exécuter un binaire d'application réel," au lieu "exécuter des binaires d'application réels".--Abdessamad J (discuter) 6 janvier 2017 à 16:45 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 17:14 (CET)

Haskell forme un pont entre les équipes améliorant ... => la phrase n'est pas complète (entre les équipes et quoi?) ou mal formée.--Abdessamad J (discuter) 6 janvier 2017 à 16:45 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 17:14 (CET)

Models checkeur

Il vaut mieux je pense comme j'avais signalé le titre "Models checkeur" en français.--Abdessamad J (discuter) 6 janvier 2017 à 16:53 (CET)

fait--LahceneTiir (discuter) 6 janvier 2017 à 17:28 (CET)

La phrase "Le comportement ... sont Exprimé par TLC." est mal formée avec des erreurs d'orthographe.--Abdessamad J (discuter) 6 janvier 2017 à 16:53 (CET)

fait --LahceneTiir (discuter) 6 janvier 2017 à 17:28 (CET)

Exemple d'OS formellement prouvés

SeL4

• Manque d'un lien wiki vers sel4 existe sous le nom Micronoyau L4.--Abdessamad J (discuter) 6 janvier 2017 à 16:58 (CET)

y'a pas un lien wiki qui pointe vers une page Sel4 par contre on a mis un lien wiki vers la page du micronoyeau L4 même si on préfère ne pas en mettre un car c'est pas bien expliqué , c'est pour cela on amis une référence plus détaillé vers un document qui parle du Sel4--Simo.93 (discuter) 8 janvier 2017 à 14:24 (CET)

Intérêts de la vérification formelle d'OS

Sécurité

• Je pense qu'il faut faire une note pour expliquer c'est quoi l'approche MILS ?.--Abdessamad J (discuter) 6 janvier 2017 à 17:05 (CET)
• De préférence avoir un lien wiki vers hyperviseur.--Abdessamad J (discuter) 6 janvier 2017 à 17:05 (CET)

fait --Narjis.taou (discuter) 8 janvier 2017 à 15:02 (CET)

• Cette phrase n'est pas claire et mal formée "ainsi que les systèmes qui exigent l'utilisation de langages de type sécurisé Tous les codes".--Abdessamad J (discuter) 6 janvier 2017 à 17:19 (CET)

il y avait une petite erreur de virgule --Narjis.taou (discuter) 8 janvier 2017 à 15:07 (CET)

• Cette phrase "Ceci peut être ... par le programmeur." est confuse, peut être vaut mieux de la reformuler pour mieux comprendre l'idée.--Abdessamad J (discuter) 6 janvier 2017 à 17:19 (CET)

phrase relu merci de ta contribution --Narjis.taou (discuter) 8 janvier 2017 à 15:09 (CET)

• En tant que tel => je pense manque "le" dans tel puisque vous parlez sur sel4 que vous avez désigné comme une plateforme.--

le mot en tant que tel remplace Sel4 donc pas la peine de le cité à nouveau --Narjis.taou (discuter) 8 janvier 2017 à 15:10 (CET)

Abdessamad J (discuter) 6 janvier 2017 à 17:24 (CET)

• ... qui permettra la construction de systèmes ... => de préférence conjuguer le verbe "permettre" au présent.--

fait --Narjis.taou (discuter) 8 janvier 2017 à 15:12 (CET)Abdessamad J (discuter) 6 janvier 2017 à 17:24 (CET)

• ... tels que l'exécution sûre ... => je pense "tels" doit être "telle" (une exécution).--Abdessamad J (discuter) 6 janvier 2017 à 17:29 (CET)

fait --Narjis.taou (discuter) 8 janvier 2017 à 15:14 (CET)

• ... La technique utilisé pour la vérification => manque "e" dans "utilisé".--Abdessamad J (discuter) 6 janvier 2017 à 17:29 (CET)

fait--Narjis.taou (discuter) 8 janvier 2017 à 15:18 (CET)

• Le paragraphe qui commence par "La technique utilisée" n'est pas clair et mal formé avec des erreurs d'orthographes.--Abdessamad J (discuter) 6 janvier 2017 à 17:39 (CET)

paragraphe relu merci de ta contribution --Narjis.taou (discuter) 8 janvier 2017 à 15:02 (CET)

Coûts

• Je pense qu'il vaut mieux faire des notes pour ACL2, Coq, PVS, HOL.--Abdessamad J (discuter) 6 janvier 2017 à 17:56 (CET)
• il y a des phrases mal formulées et incompréhensibles comme La phrase "Des assistants ... réussies"--Abdessamad J (discuter) 6 janvier 2017 à 17:56 (CET)

fait --Narjis.taou (discuter) 8 janvier 2017 à 21:20 (CET)

Historique

• Je pense que ce n'est pas la peine de mettre ?, soit on connaît la date on la met sinon on ne met pas, l’essentiel il faut préciser.--Abdessamad J (discuter) 6 janvier 2017 à 17:56 (CET)

Je pense qu'il faut tout de même le mettre. Car même si on ne connait pas la date (de début ou de fin), on a au moins une idée de la période pendant laquelle c'est déroulé le projet.--Loik D./Tiir IIR (discuter) --Tiir IIR (discuter)--Tiir IIR (discuter)--Tiir IIR (discuter)--Tiir IIR (discuter) 11 janvier 2017 à 10:41 (CET)

Note

• De préférence avoir une section pour les notes

Deuxième lecture du 06/01/2017 pour le Fond - Abdessamad J.

Bonjour, je me permet de vous relire pour une deuxième fois pour faire des remarques sur le fond de vos articles :

Bonjour je vous remercie pour ces remarques aux quelles on va essayer de vous répondre. Cordialement --LahceneTiir (discuter) 8 janvier 2017 à 06:54 (CET)

Généralités

Définitions

Système d'exploitation

Vous avez dit n’importe quel code informatique, peut être convertit mathématiquement, mais vous n'avez pas donnée un exemple.--Abdessamad J (discuter) 6 janvier 2017 à 18:46 (CET)

On a bien donné un exemple de micronoyau seL4.--LahceneTiir (discuter) 8 janvier 2017 à 06:49 (CET)

Méthodes de vérifications

• Dans cette partie je trouve que vous avez parlé sur ces méthodes sans prouver leur efficacité.(montrer des recherches, des résultats qui ont étés faites sur l'efficacité de ces méthodes) --Abdessamad J (discuter) 6 janvier 2017 à 18:46 (CET)

le but de cette partie c'est de citer quelques méthodes, et pas rentré dans les détails car cela est un autre sujet à Aborder --Narjis.taou (discuter) 8 janvier 2017 à 20:51 (CET)

Preuve par le code

• Ici vous avez juste mentionner les frameworks type PCC conventionnel, PCC fondationel sans parler sur la particularité de chaque type et comment ils peuvent vérifient une preuve mathématique ?--Abdessamad J (discuter) 6 janvier 2017 à 18:46 (CET)
• Vous avez cité un point négatif sur cette méthode sans dire s'il y a des points positifs ou non si oui il faut les dire comme vous avez mentionné le point négatif.--Abdessamad J (discuter) 6 janvier 2017 à 18:46 (CET)

Critères communs

• Vous critiquez les méthodes formelles avant de montrer leurs intérêts, je pense qu'il faut faire l'inverse.--Abdessamad J (discuter) 6 janvier 2017 à 18:46 (CET)

Effectivement, j'ai modifié cela.--Loik D./Tiir IIR (discuter) 10 janvier 2017 à 14:13 (CET)

Remarque générale

Je pense que le sujet manque des points importants comme :

• de montrer l’intérêt des systèmes formellement prouvés.--Abdessamad J (discuter) 6 janvier 2017 à 19:17 (CET)
• de dire s'il y a des risques pendant la vérification formelle du système--Abdessamad J (discuter) 6 janvier 2017 à 19:01 (CET)

veuillez lire s'il vous plait la partie critères communs. Merci --Narjis.taou (discuter) 8 janvier 2017 à 21:17 (CET)

oui je l'ai déjà bien lu moi je parle sur l’intérêt de prouver les systèmes même dans la vie de l'entreprise, et non pas l’intérêt de la vérification des systèmes.--Abdessamad J (discuter) 11 janvier 2017 à 10:52 (CET)