Grande Salle de VERIMAG
7 mai 2010 - 14h00
Vérification automatique de modèles de systèmes sur puce
par Kevin Marquet de 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.
