Anna Philippou

Kamila Barylska, Anna Gogolinska, Lukasz Mikulski et al.

Reversible computation is an emerging computing paradigm that allows any sequence of operations to be executed in reverse order at any point during computation. Its appeal lies in its potential for lowpower computation and its relevance to a wide array of applications such as chemical reactions, quantum computation, robotics, and distributed systems. Reversing Petri nets are a recently-proposed extension of Petri nets that implements the three main forms of reversibility, namely, backtracking, causal reversing, and out-of-causal-order reversing. Their distinguishing feature is the use of named tokens that can be combined together to form bonds. Named tokens along with a history function, constitute the means of remembering past behaviour, thus, enabling reversal. In recent work, we have proposed a structural translation from a subclass of RPNs to the model of Coloured Petri Nets (CPNs), an extension of traditional Petri nets where tokens carry data values. In this paper, we extend the translation to handle RPNs with token multiplicity under the individual-token interpretation, a model which allows multiple tokens of the same type to exist in a system. To support the three types of reversibility, tokens are associated with their causal history and, while tokens of the same type are equally eligible to fire a transition when going forward, when going backwards they are able to reverse only the transitions they have previously fired. The new translation, in addition to lifting the restriction on token uniqueness, presents a refined approach for transforming RPNs to CPNs through a unifying approach that allows instantiating each of the three types of reversibility. The paper also reports on a tool that implements this translation, paving the way for automated translations and analysis of reversible systems using CPN Tools.

Evangelia Vanezi, Georgia M. Kapitsaki, Anna Philippou

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.

Dimitrios Kouzapas, Anna Philippou

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 $π$-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.