The application of the General Data Protection Regulation (GDPR) has significantly affected privacy requirements elicitation, modelling, and verification in Software Engineering (SE). One of the affected areas is requirements visualisation through modelling diagrams, which plays a crucial role in ensuring privacy compliance, as functional system requirements should be integrated with GDPR-based privacy requirements. We present a systematic literature review on how SE diagrams have been employed to capture and integrate GDPR-based privacy requirements into software system design. The study aims to identify the existing research landscape, existing gaps, and directions for future work. Following a rigorous search protocol and addressing two research questions, 18 primary studies published between 2017 and 2025 were selected, analysed, and categorised based on (i) the diagram types used, and (ii) the GDPR principles or rights addressed. The findings highlight the need for inter-diagram integration, full lifecycle traceability mechanisms, tool support, and automated compliance checking.

The notion of processing purpose , as set out in the EU General Data Protection Regulation (GDPR), comprises a crucial part of a software system’s privacy policy. Processing purposes are meant to characterize the usage of personal data within a system. In this work, we propose a formal type language for defining purposes as the communication exchanges between a system’s entities, based on session types enhanced with privacy notions. In order to provide software engineers with the means to easily define processing purposes, we encode the formal language syntax to a UML-based domain model and we present DiálogoP, a tool that supports the graphical model definition and subsequently translates it into formal language definitions.

Since the adoption of the EU General Data Protection Regulation (GDPR) in May 2018, designing software systems that conform to the GDPR principles has become vital. Modeling languages can be a facilitator for this process, following the principles of model-driven development. In this paper, we present our work on the usage of a π-calculus-based language for modeling and reasoning about the GDPR provisions of 1) lawfulness of processing by providing consent, 2) consent withdrawal, and 3) right to erasure. A static analysis method based on type checking is proposed to validate that a model conforms to associated privacy requirements. This is the first step towards a rigorous Privacy-By-Design methodology for analyzing and validating a software system model against the GDPR. A use case is presented to discuss and illustrate the framework.

The European Union General Data Protection Regulation (GDPR) governs personal data processing, aiming to ensure privacy in all systems handling such data. All systems that process personal data, including software systems are legally obliged to comply to all articles of the GDPR applicable to them. In this paper, the case study of an e-Learning software platform, namely the INFORM platform and its compliance to relevant articles of the GDPR is presented. The e-Learning platform was developed with the objective to host the educational material developed under the JUSTICE EU-funded project INFORM, targeting judiciary, court staff and legal practitioners, in order to provide free and open distance access to the content. In particular, the paper demonstrates the compliance of the platform with the articles and principles of: Data Minimisation, Lawfulness of Processing, Right to Erasure, Right of Access, Right to Data Portability, Right to Rectification and Security of Processing. By applying these articles, conformance to the provision for Data Protection by design is also achieved; the platform's software development process integrates the articles of the GDPR early in the development steps, from the specification and design phases. We show how the design process progressed and demonstrate the corresponding functionality within the e-Learning platform. The paper extracts a list of lessons learned and conclusions on software GDPR compliance.

In this paper we propose a formal framework for studying privacy in information systems. The proposal follows a two-axes schema where the first axis considers privacy as a taxonomy of rights and the second axis involves the ways an information system stores and manipulates information. We develop a correspondence between the above schema and an associated model of computation. In particular, we propose the \Pcalc, a calculus based on the $\pi$-calculus with groups extended with constructs for reasoning about private data. The privacy requirements of an information system are captured via a privacy policy language. The correspondence between the privacy model and the \Pcalc semantics is established using a type system for the calculus and a satisfiability definition between types and privacy policies. We deploy a type preservation theorem to show that a system respects a policy and it is safe if the typing of the system satisfies the policy. We illustrate our methodology via analysis of two use cases: a privacy-aware scheme for electronic traffic pricing and a privacy-preserving technique for speed-limit enforcement. Comment: 43 pages

In this paper we consider the frameworks of Process Algebra and I/O Automata and we apply both towards the verification of a distributed leader-election protocol. Based on the two experiences we evaluate the approaches and draw initial conclusions with respect to their relative capabilities, strengths and usability.To the best of our knowledge, this is the first hands-on evaluation of the two models, and we view it as the cornerstone for a wider investigation of the strengths and weaknesses of the two methodologies in specifying and verifying (distributed) protocols.

We study the problem of selfish routing in the presence of incomplete network information. Our model consists of a number of users who wish to route their traffic on a network of m parallel links with the objective of minimizing their latency. However, in doing so, they face the challenge of lack of precise information on the capacity of the network links. This uncertainty is modelled via a set of probability distributions over all the possibilities, one for each user. The resulting model is an amalgamation of the KP-model of (E. Koutsoupias and C. H. Papadimitriou, 1999) and the congestion games with user-specific functions of (I. Milchtaich, 1996). We embark on a study of Nash equilibria and the price of anarchy in this new model. In particular, we propose polynomial-time algorithms for computing some special cases of pure Nash equilibria and we show that negative results of (I. Milchtaich, 1996), for the non-existence of pure Nash equilibria in the case of three users, do not apply to our model. Consequently, we propose an interesting open problem in this area, that of the existence of pure Nash equilibria in the general case of our model. Furthermore, we consider appropriate notions for the social cost and the price of anarchy and obtain upper bounds for the latter. With respect to fully mixed Nash equilibria, we propose a method to compute them and show that when they exist they are unique. Finally we prove that the fully mixed Nash equilibrium maximizes the social welfare.

We propose a unifying method for analysis of scheduling problems in real-time systems. The method is based on ACSR-VP, a real-time process algebra with value-passing capabilities. We use ACSR-VP to describe an instance of a scheduling problem as a process that has parameters of the problem as free variables. The specification is analyzed by means of a symbolic algorithm. The outcome of the analysis is a set of equations, a solution to which yields the values of the parameters that make the system schedulable. Equations are solved using integer programming or constraint logic programming. The paper presents specifications of two scheduling problems as examples.