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
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.
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

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⟩

Share

Metrics

Record views

407

Files downloads

169