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.
Liste complète des métadonnées

Cited literature [14 references]  Display  Hide  Download
Contributor : Wendelin Serwe <>
Submitted on : Thursday, November 17, 2011 - 10:26:43 AM
Last modification on : Thursday, October 11, 2018 - 8:48:03 AM
Document(s) archivé(s) le : Saturday, February 18, 2012 - 2:31:16 AM


Files produced by the author(s)


  • HAL Id : hal-00642029, version 1


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. ⟨hal-00642029⟩



Record views


Files downloads