Formal Specification and Boundary Objects: A Two-Layered Approach to GDPR Specification

Specification remains a major bottleneck for formal verification, all the more when it comes to non-functional properties or if the specification has to be understood by non-technical stakeholders. In this paper, we investigate formal specification from the perspective of boundary objects. A boundary object is an artifact that enables to create a shared understanding between different groups, which is a core property for auditing of code, where developers must demonstrate that they implemented the intended behaviour. To this end, we consider the General Data Protection Regulation, which governs the processing of personal data within the European Union. On an example program, we illustrate three different ways to express the intent to be compliant with the GDPR, and discuss how simple, informal specification can be used in auditing, while complex, formal specification lack the flexibility to act as boundary objects. We conclude with a discussion how to relate these two layers of specification formally.