Section outline

    • Ce chapitre 8 présente l'utilisation des SED dans le cadre de la vérification formelle.
      La vérification est une méthode qui permet de vérifier si une spécification est respectée par un modèle.
      Pour suivre les séquences, vous pouvez vous appuyer sur le support : UTL_Verif.pdf



    • Équipe pédagogique

      Contributeurs : Pascale Marangé, Alexandre Philippot et Olivier H. Roux
      Intervenante :  Pascale Marangé

    • Students must
      Mark as done

      Motivations pour faire de la vérification formelle


    • Students must
      Mark as done

      Vérification formelle par model-checking


    • Students must
      Mark as done

      Modélisation des propriétés


    • Mise en application
       
      A vous de mettre en application ce que vous venez d'apprendre sur un exemple en utilisant


    • Références

      Clarke E. et al (1994). Model checking and abstraction. ACM-TOPLAS,
      vol. 16, no 5.
      G. Behrmann, J. Bengtsson, A. David, K. Larsen, P. Petterson et Wang Yi.
      (2002) UPPAAL Implementation Secrets . Proc. FTRTFT 2002, Springer LNCS
      2469, pp. 3-22

    • Pour aller plus loin

      Pour aller plus loin, vous pouvez regarder la présentation du diagnostic via le chapitre 10.

    • Pour revenir en arrière

      Si les notions d'automates temporisés ne sont pas claires, vous pouvez suivre les vidéos FRM_Motivation_AjoutTemps.mp4 et FRM_Aut_T_ModelisationTemps.mp4.