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
* Corresponding author
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.
Keywords : Formal specification Language Semantics Packet filtering K framework
Document type :
Conference papers
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download
https://hal.inria.fr/hal-01401849
Contributor : Gurvan Le Guernic <>
Submitted on : Wednesday, November 23, 2016 - 7:46:14 PM
Last modification on : Thursday, February 7, 2019 - 2:59:28 PM

File

2016-08-21_F-IDE_FSPFL.pdf
Files produced by the author(s)

Identifiers

  • 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, Catherine Dubois; Dominique Mery; Paolo Masci, Nov 2016, Limassol, Cyprus. ⟨hal-01401849⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

407

Files downloads

169

Contact


archive-ouverte@inria.fr