WARNING:
JavaScript is turned OFF. None of the links on this concept map will
work until it is reactivated.
If you need help turning JavaScript On, click here.
Cette carte de concepts créée avec IHMC CmapTools traite de: 10_LOG670-H2011, des contraintes qui s'appliquent sur diagrammes de classes, spécification formelle permettent parfois de générer du code, des vérifications formelles en effectuant vérification de modèles model-checking, Réseaux de Petri permet de modéliser systèmes distribués, le comportement du système concret avec celui prévue par la spécification formelle, méthodes formelles de développement permettent de comparer le comportement du système concret, des propriétés structurelles grâce aux calcul des invariants, vérification de modèles model-checking pour la validité des propriétés, club vidéo simpliste comporte les invariants Une vidéo empruntée est nécessairement une vidéo de la banque Deux clients distincts ne peuvent avoir des vidéos en commun Le nombre d’emprunts est <= 6, des propriétés comportementales comprenant absence de blocage, calcul des invariants comprend les P-invariants, langages formels langages existants logique du 2e ordre, RdP conditions/événements CE net évolution vers RdP colorés, UPPAAL permet de modéliser systèmes réactifs/automates communiquants, vérification de modèles model-checking pour trouver des contre-exemples, UPPAAL avec langage CTL computation tree logic, RdP conditions/événements CE net évolution vers RdP places/transitions PT net, une représentation symbolique pour les graphes de transitions afin de pouvoir vérifier des systèmes très larges (avec 10^20 états), vérification de modèles model-checking qui consiste à ????, des propriétés comportementales comprenant pseudo-vivacités