Grande Salle de VERIMAG
7 May 2010 - 14h00
Vérification automatique de modèles de systèmes sur puce
by Kevin Marquet from Verimag
Résumé : La modélisation des systèmes sur puce permet de valider en avance de phase des architectures matérielles. Lors de ce séminaire je présenterai mes travaux traitant de la vérification formelle et
automatique de programmes SystemC, le standard en matière de modélisation. Je détaillerai comment une représentation formelle peut être extraite d'un tel programme parallèle. Je décrirai les avantages
d'une forme exécutable et SSA pour cette représentation intermédiaire. Je détaillerai une sémantique SystemC et une traduction automatique vers le model-checker SPIN. Je donnerai également les
résultats préliminaires de l'interprétation abstraite de programmes SystemC.
