Aujourd'hui, de nombreux systèmes à base de composants sont critiques ; leur fonctionnement requiert un niveau de confiance maximal. Cette thèse propose un cadre de description haut niveau, où la vérification accompagne la modélisation du système, et limite le problème de l'explosion combinatoire du model checkingp par une vérification modulaire des composants du système. L'approche se base sur les observateurs, qui s'exécutent en parallèle d'un système sans en modifier le comportement global et permettent de décrire des propriétés. La modularité de la vérification vient de la possibilité de remplacer avec sureté tout ou partie d'un système par un autre. Ceci est rendu possible par l'utilisation conjointe du model checking et de l'interprétation abstraite, ce qui assure le calcul d'un sur-ensemble des comportements du système. Alors que l'interprétation abstraite introduit des approximations, les observateurs permettent de distinguer des états qui auraient été fusionnés pour gagner la précision nécessaire. Ils pilotent les analyses en introduisant des instants d'observation. Décrits par l'utilisateur, ils permettent une mise au point interactive des états à fusionner.
Il n'y a pas encore de discussion sur ce livre
Soyez le premier à en lancer une !
"On n'est pas dans le futurisme, mais dans un drame bourgeois ou un thriller atmosphérique"
L'auteur se glisse en reporter discret au sein de sa propre famille pour en dresser un portrait d'une humanité forte et fragile
Au Rwanda, l'itinéraire d'une femme entre rêve d'idéal et souvenirs destructeurs
Participez et tentez votre chance pour gagner des livres !
