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

Gurvan Le Guernic 1, 2 José Angel Galindo Duarte 2
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 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. In the context of this experimentation, the cost and benefits of formally specifying a language using a tool-supported framework in general (as well as the expressivity and ease of use of the K framework in particular) are evaluated.
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01385541
Contributor : Gurvan Le Guernic <>
Submitted on : Friday, October 21, 2016 - 3:24:15 PM
Last modification on : Thursday, February 7, 2019 - 4:49:01 PM

File

RR-8967.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NonCommercial - NoDerivatives 4.0 International License

Identifiers

  • HAL Id : hal-01385541, version 1

Citation

Gurvan Le Guernic, José Angel Galindo Duarte. Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework. [Research Report] RR-8967, Inria Rennes Bretagne Atlantique. 2016, pp.41. ⟨hal-01385541⟩

Share

Metrics

Record views

430

Files downloads

265