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

Gurvan Le Guernic
Benoit Combemale
José A. Galindo

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.

In Catherine Dubois, Paolo Masci and Dominique Méry: Proceedings of the Third Workshop on Formal Integrated Development Environment (F-IDE 2016), Limassol, Cyprus, November 8, 2016, Electronic Proceedings in Theoretical Computer Science 240, pp. 38–52.
Published: 27th January 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: