Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework
Programming Languages
2017-01-31 v1 Software Engineering
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
Cite
@article{arxiv.1701.08467,
title = {Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework},
author = {Gurvan Le Guernic and Benoit Combemale and José A. Galindo},
journal= {arXiv preprint arXiv:1701.08467},
year = {2017}
}
Comments
In Proceedings F-IDE 2016, arXiv:1701.07925