Verification of an Industrial SystemC/TLM Model using LOTOS and CADP

Hubert Garavel 1 Claude Helmstetter 1 Olivier Ponsini 1 Wendelin Serwe 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : SystemC/TLM is a widely used standard for system level descriptions of complex architectures. It is particularly useful for fast simulation, thus allowing early development and testing of the targeted software. In general, formal verification of SystemC/TLM relies on the translation of the complete model into a language accepted by a verification tool. In this paper, we present an approach to the validation of a SystemC/TLM description by translation into LOTOS, reusing as much as possible of the original SystemC/TLM C++ code. To this end, we exploit a feature offered by the formal verification toolbox CADP, namely the import of external C code in a LOTOS model. We report on experiments of our approach on the BDisp, a complex graphical processing unit designed by STMicroelectronics.
Type de document :
Communication dans un congrès
7th ACM-IEEE International Conference on Formal Methods and Models for Codesign MEMOCODE'2009, Jul 2009, Cambridge, MA, United States. 2009
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00408283
Contributeur : Christine Mckinty <>
Soumis le : jeudi 30 juillet 2009 - 10:19:39
Dernière modification le : mercredi 11 avril 2018 - 01:55:43
Document(s) archivé(s) le : mardi 15 juin 2010 - 21:48:20

Fichier

Garavel-Helmstetter-Ponsini-Se...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00408283, version 1

Citation

Hubert Garavel, Claude Helmstetter, Olivier Ponsini, Wendelin Serwe. Verification of an Industrial SystemC/TLM Model using LOTOS and CADP. 7th ACM-IEEE International Conference on Formal Methods and Models for Codesign MEMOCODE'2009, Jul 2009, Cambridge, MA, United States. 2009. 〈inria-00408283〉

Partager

Métriques

Consultations de la notice

299

Téléchargements de fichiers

268