Towards automatic Maude specifications generation from C functions

Résumé

In this paper, we aim to contribute to the knowledge about how imperative C functions can be transformed to Maude functional and system modules respectively. Maude is a formal specification language characterized by simplicity, expressivity and good performance. It is a multi-paradigm meta-language based on rewriting logic and equational theories used to specify, simulate and formally verify concurrent and distributed systems. Maude has been used to define the operational semantics of many programming and specification languages. In particular, the addition of this paper is to close the gap between a subset of the C standard language and Maude relying on a transformational approach.

Citer ce document

Accès au document

Texte intégral en lecture en ligne, réservé aux abonnés SPHAERO et aux membres de l'institution. Se connecter

Voir l'article sur le site de la revue

Auteur(s)

Statistiques

Consultations : 1

Téléchargements : 0