Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit using CADP

Etienne Lantreibecq 1 Wendelin Serwe 2
2 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : The complexity of multiprocessor architectures for mobile multi-media applications renders their validation challenging. In addition, to provide the necessary flexibility, a part of the functionality is realized by software. Thus, a formal model has to take into account both hardware and software. In this paper we report on the use of LOTOS NT and CADP for the formal modeling and analysis of the DTD (Dynamic Task Dispatcher), a complex hardware block of an industrial hardware architecture developed by STMicroelectronics. Using LOTOS NT facilitated exploration of alternative design choices and increased the confidence in the DTD, by, on the one hand, automatic analysis of formal models easily understood by the architect of the DTD, and, on the other hand, co-simulation of the formal model with the implementation used for synthesis.
Type de document :
Communication dans un congrès
Formal Methods for Industrial Critical Systems, 2011, Trento, Italy. 2011
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00642029
Contributeur : Wendelin Serwe <>
Soumis le : jeudi 17 novembre 2011 - 10:26:43
Dernière modification le : jeudi 11 octobre 2018 - 08:48:03
Document(s) archivé(s) le : samedi 18 février 2012 - 02:31:16

Fichier

Lantreibecq-Serwe-11.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00642029, version 1

Citation

Etienne Lantreibecq, Wendelin Serwe. Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit using CADP. Formal Methods for Industrial Critical Systems, 2011, Trento, Italy. 2011. 〈hal-00642029〉

Partager

Métriques

Consultations de la notice

437

Téléchargements de fichiers

117