EPspectra: A Formal Approach to Developing DSP Software Applications

Hahnsang Kim 1 Thierry Turletti 1 Amar Bouali 1
1 PLANETE - Protocols and applications for the Internet
Inria Grenoble - Rhône-Alpes, CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072294
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 8:19:49 PM
Last modification on : Wednesday, April 11, 2018 - 1:53:20 AM
Long-term archiving on : Sunday, April 4, 2010 - 11:02:36 PM

Identifiers

  • HAL Id : inria-00072294, version 1

Collections

Citation

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

Share

Metrics

Record views

257

Files downloads

171