Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework

Gurvan Le Guernic 1, 2, * Benoit Combemale 2 José Angel Galindo Duarte 2
* Auteur correspondant
1 DGA.MI - DGA Maîtrise de l'information
2 DiverSe - Diversity-centric Software Engineering
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Many project-specific languages, including in particular filtering languages, are defined using non-formal specifications written in natural languages. This leads to ambiguities and errors in the specification of those languages. This paper reports on an industrial experiment on using a tool-supported language specification framework (K) for the formal specification of the syntax and semantics of a filtering language having a complexity similar to those of real-life projects. This experimentation aims at estimating, in a specific industrial setting, the difficulty and benefits of formally specifying a packet filtering language using a tool-supported formal approach.
Mots-clés : Spécification Formelle Langage Sémantique Filtrage de trames Framework K
Type de document :
Communication dans un congrès
3rd Workshop on Formal Integrated Development Environment, Nov 2016, Limassol, Cyprus. Electronic Proceedings in Theoretical Computer Science (EPTCS), 2016, 〈https://sites.google.com/site/fideworkshop2016/〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01401849
Contributeur : Gurvan Le Guernic <>
Soumis le : mercredi 23 novembre 2016 - 19:46:14
Dernière modification le : jeudi 7 février 2019 - 14:59:28

Fichier

2016-08-21_F-IDE_FSPFL.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01401849, version 1

Collections

INSTITUT-TELECOM | UNIV-RENNES1 | INRIA | IRISA | CENTRALESUPELEC | UR1-UFR-ISTIC | UNIV-RENNES | IRISA-D4

Citation

Gurvan Le Guernic, Benoit Combemale, José Angel Galindo Duarte. Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework. 3rd Workshop on Formal Integrated Development Environment, Nov 2016, Limassol, Cyprus. Electronic Proceedings in Theoretical Computer Science (EPTCS), 2016, 〈https://sites.google.com/site/fideworkshop2016/〉. 〈hal-01401849〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

346

Téléchargements de fichiers

91

Contact


archive-ouverte@inria.fr