Integrating Verification of Purpose-Aware Privacy Policies into System Design for GDPR Compliance (ciclo LiMoSP)

The General Data Protection Regulation (GDPR) establishes purpose limitation as a fundamental constraint on personal data processing: data must be collected and processed strictly in accordance with explicitly defined purposes. Yet, in mainstream software engineering practice, purposes are often treated as informal declarations, disconnected from system behaviour and lacking formal guarantees. In this talk, a unified framework for purpose-aware software engineering is presented, placing Multiparty Session Types (MPSTs) at its core. Processing purposes are modelled as structured interaction protocols that describe how personal data is exchanged among system entities. System implementations are specified in a π-calculus-based modelling language, and a dedicated type system enables static verification that implementations conform to declared purposes and related GDPR requirements, including consent management and data subject rights. Formal results such as type preservation and session fidelity provide rigorous compliance guarantees. The talk further outlines how this formal foundation is integrated with purpose-aware UML use case and sequence diagrams, enabling software engineers to capture purposes as structured behavioural constructs linked to personal data flows and actor responsibilities. A prototype tool supports the visual definition of such models and their automatic translation into MPST representations for compliance checking. The framework establishes a pathway from visual requirements modelling to automated, type-based validation, advancing a practically applicable privacy-by-design methodology.