epita/notes-ing2
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
notes-ing2/surete/01_model_checking.md

2 KiB
Raw Blame History

  • modèle : représentation mathématique
  • vérification : algorithme fournissant une preuve adaptée

modèle

  • système de transitions

    • machine à état, avec des états non désirés

  • synchronicité

    • synchrone

      • opérations sur tous les circuits sont organisées par une seule horloge de manière granulaire
      • physiquement, le temps de propagation des signaux est bien inférieur à la période de l'horloge

    • asynchrone

      • des signaux peuvent se propager entre circuits avant la fin d'un changement d'état d'un circuit
      • comporte des signaux indépendants et des verroux de synchronisation
      • exemple : échanges réseau, composants à plusieurs horloges

  • transition

    • synchrone : une transition change tous les circuits
    • asynchrone : une transition ne concerne et change qu'un circuit

automate fini

  • ensemble d'état

  • ensemble de transitions

  • un 'langage' qui sert d'entrées système

  • une phrase qui est une entrée précise

  • les état finaux serviront de cas d'erreurs, nous cherchons donc à vérifier que l'état final ne peut pas être atteint

  • on peut différencier des langages pour analyser un sous ensemble de cas à vérifier lorsqu'on intègre de nouvelles entrées

  • faire le produit d'automates A et B, c'est former l'automate qui prends comme transition les tuples des entrées de A et B

Exemple

propriété : tout A est suivi d'un B dans le langage (b+ab)*

structure de kripke

  • défini par une liste de propositions
  • ensemble de variables propositionnelles (équation booléennes)
  • ensemble d'états
  • ensemble de transitions
  • pour chaque état, l'ensemble des propositions qui sont vérifiées par cet état

traces

  • suite d'évènements / états

  • est un ensemble mathématique de la forme:

    • toutes les suites avec :
      • e_0 est un état de départ
      • (e_n, e_n+1) est une transition existante

  • arborescence

    • arbre des états possibles en arrivant à chaque état en partant de l'état initial
      • racine : état de départ
      • enfants d'un neud : états accessibles depuis cet état