Formal Analysis of a Hardware Dynamic Task Dispatcher with CADP

Etienne Lantreibecq 1 Wendelin Serwe 2, *
* Auteur correspondant
2 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : The complexity of multiprocessor architectures for mobile multimedia 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 article we report on the use of the CADP toolbox for the formal modeling and analysis of the DTD (Dynamic Task Dispatcher), a complex hardware block of an industrial hardware architecture developed by STMicroelectronics. The formal LNT model developed by an industry engineer was appropriate to discuss implementation details with the architect and enabled model-checking temporal properties expressed in MCL, which discovered a possible problem. We investigated the existence of the problem in the architect's C++ model using co-simulation of the C++ and the formal LNT models.
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00782069
Contributeur : Wendelin Serwe <>
Soumis le : mardi 29 janvier 2013 - 09:52:44
Dernière modification le : jeudi 11 janvier 2018 - 06:23:43
Document(s) archivé(s) le : mardi 30 avril 2013 - 03:57:03

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Etienne Lantreibecq, Wendelin Serwe. Formal Analysis of a Hardware Dynamic Task Dispatcher with CADP. Science of Computer Programming, Elsevier, 2014, 80, pp.130-149. 〈10.1016/j.scico.2013.01.003〉. 〈hal-00782069〉

Partager

Métriques

Consultations de la notice

350

Téléchargements de fichiers

190