EPspectra: A Formal Approach to Developing DSP Software Applications - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2001

EPspectra: A Formal Approach to Developing DSP Software Applications

Résumé

Software approach to developing Digital Signal Processing (DSP) applications brings some interesting features, such as flexibility, re-usability of resources and easy upgrades of applications. However, it requires long tests and verification phases due to the increasing complexity of software. In this report, we present the EPspectra toolkit, an Esterel-based developmen- t verification environment targeted to develop DSP applications on general purpose computers. We illustrate the description with an example of DSP implementation: the radio interface part of a GSM base station. Such DSP applications have complex control-paths since they have to obey strict scheduling rules. The purpose of the Esterel formal method is to ease the programming of complex control-paths and the verification of safety properties of these control-paths. In this report, we show how we verify several critical safety properties of the radio interface of our GSM using the Esterel verification environment. Since the model used for the executable code generation and for the formal verification is the same, the EPspectra toolkit achieves the faithful verification of the targeted application. By using EPspectra, we obtain a higher confidence in the final implementation since traditional verification techniques based on simulation and testing can only partially verify the program.Moreover, the EPspectra approach has shown the drastic reduction of verification/testing time while requiring relatively few expertise in formal language verification methods.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-4293.pdf (298.21 Ko) Télécharger le fichier
Loading...

Dates et versions

inria-00072294 , version 1 (23-05-2006)

Identifiants

  • HAL Id : inria-00072294 , version 1

Citer

Hahnsang Kim, Thierry Turletti, Amar Bouali. EPspectra: A Formal Approach to Developing DSP Software Applications. [Research Report] RR-4293, INRIA. 2001. ⟨inria-00072294⟩
98 Consultations
96 Téléchargements

Partager

Gmail Facebook X LinkedIn More