AI 中文总结
针对GDPR中个人数据处理需按明确目的进行但实践中目的与系统行为脱节的问题，引入基于多方会话类型的正式框架，用进程演算和类型系统验证目的合规性，通过案例研究展示方法，旨在发展为统一目的建模与验证的软件工程方法。
AI 中文摘要
通用数据保护条例（GDPR）将目的限制确立为个人数据处理的基本约束：个人数据必须严格按照明确指定的目的进行收集、存储和处理。然而在主流软件工程实践中，目的常被视为非正式声明，与系统行为脱节。在分布式系统中这一差距问题尤甚。基于此，我们引入基于多方会话类型的正式、目的感知框架，用进程演算指定系统实现，定义类型系统验证合规性，并通过医疗系统案例研究展示方法，目标是将其发展为统一目的建模和合规验证的软件工程方法。
英文摘要
The General Data Protection Regulation (GDPR) establishes purpose limitation as a fundamental constraint on personal data processing: personal data must be collected, stored, and processed strictly in accordance with explicitly specified purposes. Therefore, systems are required not only to declare the purposes under which personal data are processed, but also to ensure that their runtime behaviour remains aligned with the declared purposes. Yet, in mainstream software engineering practice, purposes are often treated as informal declarations, largely disconnected from system behaviour and, therefore, not amenable to rigorous reasoning about purpose compliance. This gap becomes particularly problematic in distributed systems, where personal data may flow across multiple entities and evolve through complex communication patterns. To address this challenge, recent works propose a more elaborate treatment of purposes based on structured, action-oriented representations of the data-processing interactions involved in their fulfilment. Building on these insights, we introduce a formal, purpose-aware framework grounded in multiparty session types in which purposes are modelled as structured interaction protocols among system entities. Within our framework, system implementations are specified using a process calculus that captures the semantics of distributed interactions and features private data as a first-class entity. Furthermore, we define a type system that verifies compliance between declared purposes and system models, and we establish subject reduction and purpose fidelity results, thereby ensuring that well-typed systems do not deviate from their specified purposes during execution. We demonstrate our approach through a case study involving a healthcare system. Ultimately, our objective is to evolve this formal framework into a software-engineering-oriented approach that unifies purpose modelling and compliance verification within a lifecycle-driven methodology, thus enabling a practically applicable privacy-by-design process.
CommentsIn Proceedings LSFA 2026, arXiv:2607.15904
Journal refEPTCS 449, 2026, pp. 259-277
