HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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 :
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 8:19:49 PM
Last modification on : Friday, February 4, 2022 - 3:16:43 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:02:36 PM


  • HAL Id : inria-00072294, version 1



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



Record views


Files downloads