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

## TL;DR

This paper reports on an industrial experiment using the K framework to formally specify a packet filtering language, aiming to evaluate the approach's difficulty and benefits in a real-world setting.

## Contribution

It demonstrates the practical application of the K framework for formal specification of complex filtering languages in an industrial context.

## Key findings

- Formal specification reduces ambiguities in language design
- Tool support facilitates understanding and correctness
- The approach is feasible for real-world projects

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