Silvia Lizeth Tapia Tarifa

• Kobialka, Paul; Pferscher, Andrea; Aichernig, Bernhard K.; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2026). Automata Learning Versus Process Mining: The Case for User Journeys. IEEE Transactions on Software Engineering. ISSN 0098-5589. 52(6), p. 1858–1874. doi: 10.1109/tse.2026.3679253. Full text in Research Archive Show summary

  With the servitization of business, understanding how users experience services becomes a crucial success factor for companies. Therefore, there is a need to include feedback from user experiences in the software engineering process. Behavioral models of user journeys, describing how users experience their interaction with a service, can provide insights and potentially improve services. In this paper, we investigate techniques that allow the automatic generation of behavioral models from user interactions with a service, recorded in an event log. We first compare two established techniques that generate behavioral models from a given event log: automata learning and process mining. Afterward, we present a novel, hybrid method that combines both automata learning and process mining methods to overcome their limitations. For the existing techniques, we present methods to learn models of user journeys and evaluate the accuracy of the resulting models. We then compare these techniques with our novel method for the automatic extraction of user journey models from the event logs of digital services. We assess the practical applicability of all techniques by evaluating real-world applications. Our results show that process mining techniques rely on expert knowledge, while automata learning techniques depend on the distribution of events in the given event log. We further show that the proposed hybrid technique combines the strengths of both process mining and automata learning, automatically selecting the best method and parameter settings for a given event log to learn very accurate models.

• Kamburjan, Eduard; Bencomo, Nelly; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2026). Declarative Lifecycle Management for Self-Adaptive Systems. Software and Systems Modeling (SoSyM). ISSN 1619-1366. doi: 10.1007/s10270-026-01358-w. Full text in Research Archive Show summary

  Self-adaptive systems can be realised as layered systems with a feedback loop: a managing system monitors a managed system, updates an internal model, and adjusts the managed system by means of controllers to maintain given requirements. For example, a digital twin coupled with its physical twin constitute such a self-adaptive system. As the managed system shifts between different stages in its lifecycle, these requirements, as well as the associated analysers and controllers, may need to change. The exact triggers for such shifts in a managed system are often hard to predict: they may be difficult to describe or even unknown. However, the shifts can generally be observed once they have occurred, in terms of changes in the system behaviour. This paper proposes an automated method for self-adaptation in self-adaptive systems to address shifts between lifecycle stages in a managed system. Our method is based on declarative descriptions of lifecycle stages for assets in a managed system and their associated counterparts in the managing system. Declarative lifecycle management provides a high-level, flexible method of self-adaptation for self-adaptive systems to reflect disruptive shifts between stages in a managed system.

• Kobialka, Paul; Johnsen, Einar Broch; Mannhardt, Felix & Tarifa, Silvia Lizeth Tapia (2025). Decision boundaries in user journey event logs. Process Science - Business Process Management and Process Mining. 2. doi: 10.1007/s44311-025-00026-4. Full text in Research Archive Show summary

  Service providers may systematically record and analyze how users interact with a service. User journeys model this interaction from the user’s perspective. We can think of user journeys in terms of multi-party event logs in which events are triggered by two independent parties, the user and the service provider, both controlling their share of actions. Multi-party event logs enable the automated construction of weighted two-player games, which can be used to analyze the user journeys. However, the games constructed for complex user journeys may get large, which makes visual understanding challenging. To reduce the size of these games, we develop an analysis technique for a game’s decision boundary, at which the outcome of the game is determined. Decision boundaries identify subgames that are equivalent to the full game with respect to the final outcome of user journeys. The paper formalizes decision boundaries for user journey games with history refinements, and studies properties of decision boundaries that simplify their analysis. The decision boundary analysis from multi-party event logs has been implemented in a modular tool, which can be connected to existing process mining pipelines, and evaluated on benchmark event logs revealing changes in the user journey and the interaction between users and service provider.

• Kløvstad, Åsmund Aqissiaq Arild; Kobialka, Paul; Sieve, Riccardo; Pferscher, Andrea; Slaughter, Laura Ann & Tarifa, Silvia Lizeth Tapia [Show all 7 contributors for this article] (2025). What-If Scenarios for the BedreFlyt Digital Twin. In Bertrand, Nathalie; Dubslaff, Clemens & Klüppelholz, Sascha (Ed.), Principles of Formal Quantitative Analysis: Essays Dedicated to Christel Baier on the Occasion of Her 60th Birthday. Springer Nature. ISSN 9783031974397. p. 360–381. doi: 10.1007/978-3-031-97439-7_18. Full text in Research Archive Show summary

  Digital twin technology is emerging as a valuable tool for both short-term decision-making and long-term strategic planning across domains such as process industry, energy, space, transport, and healthcare. This paper reports on ongoing work in designing a digital twin to enhance resource planning in hospitals, e.g., for in-patient needs. Our focus here is on a novel technique to express what-if scenarios in digital twins to improve strategic planning processes, spanning, e.g., average-case and worst-case resource needs, expected patient treatments, and ranging over variations in available resources such as bed bays in the hospital ward. Due to the modularity of our digital twin architecture, different what-if scenarios can be explored simply by configuring the digital twin’s orchestrator, which triggers a formal methods analysis pipeline that combines executable formal models for simulation, optimization over constraints and a knowledge base that formalizes domain knowledge. We illustrate what-if scenario analysis in our digital twin architecture by considering the problem of bed bay allocation in a hospital ward.

• Sieve, Riccardo; Kobialka, Paul; Slaughter, Laura Ann; Schlatte, Rudolf; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2025). BedreFlyt: Improving Patient Flows through Hospital Wards with Digital Twins. Proceedings of the First International Workshop on Autonomous Systems Quality Assurance and Prediction with Digital Twins. doi: 10.48550/ARXIV.2505.06287. Full text in Research Archive
• Pässler, Juliane Linda; Beek, Maurice H. ter; Damiani, Ferruccio; Dubslaff, Clemens; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2025). Feature-Oriented Modelling and Analysis of a Self-Adaptive Robotic System. Formal Aspects of Computing. ISSN 0934-5043. doi: 10.1145/3709159. Full text in Research Archive Show summary

  Improved autonomy in robotic systems is needed for innovation in, e.g., the marine sector. Autonomous robots that are let loose in hazardous environments, such as underwater, need to handle uncertainties that stem from both their environment and internal state. While self-adaptation is crucial to cope with these uncertainties, bad decisions may cause the robot to get lost or even to cause severe environmental damage. Autonomous, self-adaptive robots that operate in uncontrolled environments full of uncertainties need to be reliable! Since these uncertainties are hard to replicate in test deployments, we need methods to formally analyse self-adaptive robots operating in uncontrolled environments. In this paper, we show how feature-oriented techniques can be used to formally model and analyse self-adaptive robotic systems in the presence of such uncertainties. Self-adaptive systems can be organised as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of an autonomous underwater vehicle (AUV) for pipeline inspection, in which the managed subsystem of the AUV is modelled as a family of systems, where each family member corresponds to a valid configuration of the AUV which can be seen as an operating mode of the AUV’s behaviour. The managing subsystem of the AUV is modelled as a control layer that is capable of dynamically switching between such valid configurations, depending on both environmental and internal uncertainties. These uncertainties are captured in a probabilistic and highly configurable model. Our modelling approach allows us to exploit powerful formal methods for feature-oriented systems, which we illustrate by analysing safety properties, energy consumption, and multi-objective properties, as well as performing parameter synthesis to analyse to what extent environmental conditions affect the AUV. The case study is realised in the probabilistic feature-oriented modelling language and verification tool ProFeat, and in particular exploits family-based probabilistic and parametric model checking.

• Kobialka, Paul; Gerlach, Lina; Leofante, Francesco; Ábrahám, Erika; Tarifa, Silvia Lizeth Tapia & Johnsen, Einar Broch (2025). Counterfactual Strategies for Markov Decision Processes. IJCAI International Joint Conference on Artificial Intelligence. ISSN 1045-0823. 34, p. 412–420. doi: 10.24963/ijcai.2025/47. Full text in Research Archive Show summary

  Counterfactuals are widely used in AI to explain how minimal changes to a model’s input can lead to a different output. However, established methods for computing counterfactuals typically focus on one-step decision-making, and are not directly applicable to sequential decision-making tasks. This paper fills this gap by introducing counterfactual strategies for Markov Decision Processes (MDPs). During MDP execution, a strategy decides which of the enabled actions (with known probabilistic effects) to execute next. Given an initial strategy that reaches an undesired outcome with a probability above some limit, we identify minimal changes to the initial strategy to reduce that probability below the limit. We encode such counterfactual strategies as solutions to non-linear optimization problems, and further extend our encoding to synthesize diverse counterfactual strategies. We evaluate our approach on four real-world datasets and demonstrate its practical viability in sophisticated sequential decision-making tasks.

• Boer, Frank de; Johnsen, Einar Broch; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2025). Inside Every Multithreaded Program There Are Active Objects Struggling To Get Out. In Lee, Edward A.; Mousavi, Mohammad Reza & Talcott, Carolyn (Ed.), Rebeca for Actor Analysis in Action. Springer. ISSN 9783031851339. p. 349–363. doi: 10.1007/978-3-031-85134-6_15. Full text in Research Archive
• Hähnle, Reiner; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2025). An LAGC Semantics for Timed Rebeca. In Lee, Edward A.; Mousavi, Mohammad Reza & Talcott, Carolyn (Ed.), Rebeca for Actor Analysis in Action. Springer. ISSN 9783031851339. p. 326–348. doi: 10.1007/978-3-031-85134-6_14. Full text in Research Archive
• Silva, Gustavo Rezende; Pässler, Juliane Linda; Tarifa, Silvia Lizeth Tapia; Johnsen, Einar Broch & Corbato, Carlos Hernández (2025). ROSA: a knowledge-based solution for robot self-adaptation. Frontiers in Robotics and AI. 12. doi: 10.3389/frobt.2025.1531743. Full text in Research Archive Show summary

  Autonomous robots must operate in diverse environments and handle multiple tasks despite uncertainties. This creates challenges in designing software architectures and task decision-making algorithms, as different contexts may require distinct task logic and architectural configurations. To address this, robotic systems can be designed as self-adaptive systems capable of adapting their task execution and software architecture at runtime based on their context. This paper introduces ROSA, a novel knowledge-based framework for RObot Self-Adaptation, which enables task-and-architecture co-adaptation (TACA) in robotic systems. ROSA achieves this by providing a knowledge model that captures all application-specific knowledge required for adaptation and by reasoning over this knowledge at runtime to determine when and how adaptation should occur. In addition to a conceptual framework, this work provides an open-source ROS 2-based reference implementation of ROSA and evaluates its feasibility and performance in an underwater robotics application. Experimental results highlight ROSA’s advantages in reusability and development effort for designing self-adaptive robotic systems.

• Baramashetru, Chinmayi; Giannini, Paola; Tarifa, Silvia Lizeth Tapia & Owe, Olaf (2025). A Type System for Data Privacy Compliance in Active Object Languages. The Art, Science, and Engineering of Programming. ISSN 2473-7321. 10(2). doi: 10.22152/programming-journal.org/2025/10/18. Full text in Research Archive Show summary

  Data protection laws such as GDPR aim to give users unprecedented control over their personal data. Compliance with these regulations requires systematically considering information flow and interactions among entities handling sensitive data. Privacy-by-design principles advocate embedding data protection into system architectures as a default. However, translating these abstract principles into concrete, explicit methods remains a significant challenge. This paper addresses this gap by proposing a language-based approach to privacy integration, combining static and runtime techniques. By employing type checking and type inference in an active object language, the framework enables the tracking of authorised data flows and the automatic generation of constraints checked at runtime based on user consent. This ensures that personal data is processed in compliance with GDPR constraints. The key contribution of this work is a type system that gather the compliance checks and the changes to users consent and integrates data privacy compliance verification into system execution. The paper demonstrates the feasibility of this approach through a soundness proof and several examples, illustrating how the proposed language addresses common GDPR requirements, such as user consent, purpose limitation, and data subject rights. This work advances the state of the art in privacy-aware system design by offering a systematic and automated method for integrating GDPR compliance into programming languages. This capability has implications for building trustworthy systems in domains such as healthcare or finance, where data privacy is crucial.

• Pässler, Juliane Linda; Beek, Maurice H. ter; Damiani, Ferruccio; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2025). A Configurable Software Model of a Self-Adaptive Robotic System. Science of Computer Programming. ISSN 0167-6423. 240. doi: 10.1016/j.scico.2024.103221. Full text in Research Archive Show summary

  Self-adaptation, meant to increase reliability, is a crucial feature of cyber-physical systems operating in uncertain physical environments. Ensuring safety properties of self-adaptive systems is of utter importance, especially when operating in remote environments where communication with a human operator is limited, like under water or in space. This paper presents a software model that allows the analysis of one such self-adaptive system, a configurable underwater robot used for pipeline inspection, by means of the probabilistic model checker ProFeat. Furthermore, it shows that the configurable software model is easily extensible to further, possibly more complex use cases and analyses.

• Pässler, Juliane Linda; Beek, Maurice H. ter; Damiani, Ferruccio; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2025). Analysing Self-Adaptive Systems as Software Product Lines. Journal of Systems and Software. ISSN 0164-1212. 222. doi: 10.1016/j.jss.2024.112324. Full text in Research Archive Show summary

  Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems (SASs) can be realised as two-layered systems, introducing a separation of concerns between the domain-specific functionalities of the system (the managed subsystem) and the adaptation logic (the managing subsystem), i.e., introducing an external feedback loop for managing adaptation in the system. We present an approach to model SASs as dynamic software product lines (SPLs) and leverage existing approaches to SPL-based analysis for the analysis of SASs. To do so, the functionalities of the SAS are modelled in a feature model, capturing the SAS’s variability. This allows us to model the managed subsystem of the SAS as a family of systems, where each family member corresponds to a valid feature configuration of the SAS. Thus, the managed subsystem of an SAS is modelled as an SPL model; more precisely, a probabilistic featured transition system. The managing subsystem of an SAS is modelled as a control layer capable of dynamically switching between these valid configurations, depending on both environmental and internal conditions. We demonstrate the approach on a small-scale evaluation of a self-adaptive autonomous underwater vehicle used for pipeline inspection, which we model and analyse with the feature-aware probabilistic model checker ProFeat. The approach allows us to analyse probabilistic reward and safety properties for the SAS, as well as the correctness of its adaptation logic.

• Boer, Frank de; Johnsen, Einar Broch; Pun, Violet Ka I & Tarifa, Silvia Lizeth Tapia (2024). Proving Correctness of Parallel Implementations of Transition System Models. ACM Transactions on Programming Languages and Systems. ISSN 0164-0925. 46(3), p. 1–50. doi: 10.1145/3660630. Full text in Research Archive Show summary

  This article addresses the long-standing problem of program correctness for programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level models expressed as transition systems. The implementation language underlying the method is based on the concurrency model of actors and active objects. The method defines program correctness in terms of a simulation relation between the transition system that specifies the program semantics of the parallel program and the transition system that is described by the correctness specification. The simulation relation itself abstracts from the fine-grained interleaving of parallel processes by exploiting a global confluence property of the concurrency model of the implementation language considered in this article. As a proof of concept, we apply our method to the correctness of a parallel simulator of multicore memory systems.

• Din, Crystal Chang; Hähnle, Reiner; Henrio, Ludovic; Johnsen, Einar Broch; Pun, Violet Ka I & Tarifa, Silvia Lizeth Tapia (2024). Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages. ACM Transactions on Programming Languages and Systems. ISSN 0164-0925. 46(1), p. 1–58. doi: 10.1145/3648439. Full text in Research Archive Show summary

  Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. We propose a novel modular semantics designed to align smoothly with program logics used in deductive verification and formal specification of concurrent programs. Our semantics separates local evaluation of expressions and statements performed in an abstract, symbolic environment from their composition into global computations, at which point they are concretised. This makes incremental addition of new language concepts possible, without the need to revise the framework. The basis is a generalisation of the notion of a program trace as a sequence of evolving states that we enrich with event descriptors and trailing continuation markers. This allows to postpone scheduling constraints from the level of local evaluation to the global composition stage, where well-formedness predicates over the event structure declaratively characterise a wide range of concurrency models. We also illustrate how a sound program logic and calculus can be defined for this semantics.

• Johnsen, Einar Broch; Kobialka, Paul; Pferscher, Andrea & Tarifa, Silvia Lizeth Tapia (2024). Nudging Strategies for User Journeys: Take a Path on the Wild Side. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 15230. doi: 10.1007/978-3-031-73751-0_6. Full text in Research Archive
• Kobialka, Paul; Pferscher, Andrea; Bergersen, Gunnar R.; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2024). Stochastic Games for User Journeys. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 14934. doi: 10.1007/978-3-031-71177-0_12. Full text in Research Archive
• Kamburjan, Eduard; Pferscher, Andrea; Schlatte, Rudolf; Sieve, Riccardo; Tarifa, Silvia Lizeth Tapia & Johnsen, Einar Broch (2024). Semantic Reflection and Digital Twins: A Comprehensive Overview. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 15240, p. 129–145. doi: 10.1007/978-3-031-73887-6_11. Full text in Research Archive
• Baramashetru, Chinmayi; Tarifa, Silvia Lizeth Tapia & Owe, Olaf (2024). Integrating Data Privacy Compliance in Active Object Languages. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 14360, p. 270–288. doi: 10.1007/978-3-031-51060-1_10. Full text in Research Archive Show summary

  As users of digitalized services are more and more required to share their personal data, it becomes increasingly important for applications to comply with users’ consent for the handling of their personal data. Ensuring compliance with such consent requires reasoning globally about both the flow of information and the interaction of different parties handling personal data. In this direction, privacy by design principles cultivate a philosophy that endorses the development of systems with built-in abilities to demonstrate compliance with data privacy to guarantee the protection of personal data. However, there is an apparent mismatch in adopting such imprecise principles into explicit design methods that support systematic solutions that integrates data privacy in system design. In this paper, we propose an integration of privacy concepts into a core active object language, to explore how the chosen privacy-aware language semantics can ensure handling of personal data according to users’ privacy consent.

• Kamburjan, Eduard; Bencomo, Nelly; Tarifa, Silvia Lizeth Tapia & Johnsen, Einar Broch (2024). Declarative Lifecycle Management in Digital Twins. In Muñoz, Paula & Garmendia, Antonio (Ed.), MODELS Companion '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems. Association for Computing Machinery (ACM). ISSN 9798400706226. p. 353–363. doi: 10.1145/3652620.3688248. Full text in Research Archive
• Kobialka, Paul; Tarifa, Silvia Lizeth Tapia; Bergersen, Gunnar R. & Johnsen, Einar Broch (2024). User journey games: automating user-centric analysis. Software and Systems Modeling (SoSyM). ISSN 1619-1366. doi: 10.1007/s10270-024-01148-2. Full text in Research Archive Show summary

  The servitization of business is moving industry to business models driven by customer demand. Customer satisfaction is connected with financial rewards, forcing companies to invest in their users’ experience. User journeys describe how users maneuver through a service. Today, user journeys are typically modeled graphically, and lack formalization and analysis support. This paper proposes a formalization of user journeys as weighted games between the user and the service provider and a systematic data-driven method to derive these user journey games from system logs, using process mining techniques. As the derived games may contain cycles, we define an algorithm to transform user journeys games with cycles into acyclic weighted games, which can be model checked using to uncover potential challenges in a company’s interactions with its users and derive company strategies to guide users through their journeys. Finally, we propose a user journey sliding-window analysis to detect changes in the user journey over time by model checking a sequence of generated games. Our analysis pipeline has been evaluated on an industrial case study; it revealed design challenges within the studied service and could be used to derive actionable recommendations for improvement.

• Baramashetru, Chinmayi; Tarifa, Silvia Lizeth Tapia & Owe, Olaf (2024). Assuring GDPR Conformance Through Language-Based Compliance, Privacy and Identity Management. Sharing in a Digital World. Springer Nature. ISSN 9783031579783. p. 46–63. doi: 10.1007/978-3-031-57978-3_4. Full text in Research Archive Show summary

  Existing legal regulations, such as the GDPR in the European Union, exert significant pressure on businesses to embed legal principles into their information systems. These legislative provisions, expertly crafted in natural language, have raised technical challenges to be GDPR compliant. In particular, formal reasoning about compliance at the level of programming code is challenging. Available alternatives, such as manual auditing, have demonstrated limited scalability, and the absence of system-level support has led to substantial penalties for businesses and a loss of control over their personal data for users. Hence, we develop an approach that intends to reconcile the existing challenges in software implications with GDPR through programming language support. We build on earlier work introducing a privacy-aware active object language and operational semantics. To demonstrate the practicality, we here present a prototype implementation within the Maude formalism, which validates our semantics and model-checks GDPR compliance properties within any given configuration. Our work is limited to certain key concepts of the GDPR that can be interpreted at the programming level. We focus on processing rights based on user consent.

• Kobialka, Paul; Schlatte, Rudolf; Bergersen, Gunnar R.; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2024). Simulating User Journeys with Active Objects. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 14360, p. 199–225. doi: 10.1007/978-3-031-51060-1_8. Full text in Research Archive Show summary

  The servitization of business makes companies increasingly dependent on providing carefully designed user experiences for their service offerings. User journeys model services from the user’s perspective, but user journeys are today mainly constructed and analyzed manually. Recent work analyzing user journeys as games enable optimal service-provider strategies to be automatically derived, assuming a restricted user behavior. Complementing this work, we here develop an actor-based modeling framework for user journeys that is parametric in user behavior and service-provider strategies, using the active-object modeling language ABS. Strategies for the service provider, such as those derived for user journey games, can be automatically imported into the framework. Our work enables prescriptive simulation-based analyses, as strategies can be evaluated and compared in scenarios with rich user behavior.

• Turin, Gianluca; Borgarelli, Andrea; Donetti, Simone; Damiani, Ferruccio; Tarifa, Silvia Lizeth Tapia & Johnsen, Einar Broch (2023). Predicting resource consumption of Kubernetes container systems using resource models. Journal of Systems and Software. ISSN 0164-1212. 203. doi: 10.1016/j.jss.2023.111750. Full text in Research Archive Show summary

  Cloud computing has radically changed the way organizations operate their Software by allowing them to achieve high availability of services at affordable cost. Containerized microservices is an enabling technology for this change, and advanced container orchestration platforms such as Kubernetes are used for service management. Despite the flourishing ecosystem of monitoring tools for such orchestration platforms, service management is still mainly a manual effort. The modeling of cloud computing systems is an essential step towards automatic management, but the modeling of cloud systems of such complexity remains challenging and, as yet, unaddressed. In fact modeling resource consumption will be a key to comparing the outcome of possible deployment scenarios. This paper considers how to derive resource models for cloud systems empirically. We do so based on models of deployed services in a formal modeling language with explicit CPU and memory resources; once the adherence to the real system is good enough, formal properties can be verified in the model. Targeting a likely microservices application, we present a model of Kubernetes developed in Real-Time ABS. We report on leveraging data collected empirically from small deployments to simulate the execution of higher intensity scenarios on larger deployments. We discuss the challenges and limitations that arise from this approach, and identify constraints under which we obtain satisfactory accuracy.

• Kamburjan, Eduard; Klungre, Vidar Norstein; Tarifa, Silvia Lizeth Tapia; Schlatte, Rudolf; Giese, Martin & Cameron, David B. [Show all 7 contributors for this article] (2023). Emerging Challenges in Compositionality and Correctness for Digital Twins. CEUR Workshop Proceedings. 3507. Full text in Research Archive Show summary

  A digital twin is an information system that analyzes the behavior of a physical or digital system by connecting streams of observations to dynamic (e.g., simulation) and static (e.g., asset management) models of this twinned system. In large-scale industrial settings, the digital twin will often need to manage a multitude of models for subsystems reflecting different engineering disciplines, vendors, etc. To analyze such complex systems, digital twins must ensure the correct composition of these models and their correct exposure to the user. For the integration and transfer of information between models, digital twins may profit from a formalization of domain knowledge using ontologies, which have proven effective to unify data models. However, it is an open challenge to formalize and verify the correctness of digital twins. This paper discusses this problem for digital twins and illustrates challenges for formal methods with a focus on the composition of heterogeneous dynamic models.

• Pässler, Juliane Linda; Beek, Maurice H. ter; Damiani, Ferruccio; Tarifa, Silvia Lizeth Tapia & Johnsen, Einar Broch (2023). Formal Modelling and Analysis of a Self-Adaptive Robotic System. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 14300, p. 343–363. doi: 10.1007/978-3-031-47705-8_18. Full text in Research Archive Show summary

  Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV’s variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.

• Kobialka, Paul; Mannhardt, Felix; Tarifa, Silvia Lizeth Tapia & Johnsen, Einar Broch (2023). Building User Journey Games from Multi-party Event Logs. Lecture Notes in Business Information Processing. ISSN 1865-1348. 468, p. 71–83. doi: 10.1007/978-3-031-27815-0_6. Full text in Research Archive Show summary

  Abstract To improve the user experience, service providers may systematically record and analyse user interactions with a service using event logs. User journeys model these interactions from the user’s perspective. They can be understood as event logs created by two independent parties, the user and the service provider, both controlling their share of actions. We propose multi-party event logs as an extension of event logs with information on the parties, allowing user journeys to be analysed as weighted games between two players. To reduce the size of games for complex user journeys, we identify decision boundaries at which the outcome of the game is determined. Decision boundaries identify subgames that are equivalent to the full game with respect to the final outcome of user journeys. The decision boundary analysis from multi-party event logs has been implemented and evaluated on the BPI Challenge 2017 event log with promising results, and can be connected to existing process mining pipelines.

• Silva, Gustavo Rezende; Pässler, Juliane Linda; Zwanepol, Jeroen; Alberts, Elvin; Tarifa, Silvia Lizeth Tapia & Gerostathopoulos, Ilias [Show all 8 contributors for this article] (2023). SUAVE: An Exemplar for Self-Adaptive Underwater Vehicles. In Rodrigues, Genaína Nunes & Pérez, Diego (Ed.), SEAMS '23: Proceedings of the 18th Symposium on Software Engineering for Adaptive and Self-Managing Systems. IEEE (Institute of Electrical and Electronics Engineers). ISSN 9781450393058. p. 181–187. doi: 10.1109/SEAMS59076.2023.00031. Full text in Research Archive Show summary

  Once deployed in the real world, autonomous underwater vehicles (AUVs) are out of reach for human supervision yet need to take decisions to adapt to unstable and unpredictable environments. To facilitate research on self-adaptive AUVs, this paper presents SUAVE, an exemplar for two-layered system-level adaptation of AUVs, which clearly separates the application and self-adaptation concerns. The exemplar focuses on a mission for underwater pipeline inspection by a single AUV, implemented as a ROS 2-based system. This mission must be completed while simultaneously accounting for uncertainties such as thruster failures and unfavorable environmental conditions. The paper discusses how SUAVE can be used with different self-adaptation frameworks, illustrated by an experiment using the Metacontrol framework to compare AUV behavior with and without self-adaptation. The experiment shows that the use of Metacontrol to adapt the AUV during its mission improves its performance when measured by the overall time taken to complete the mission or the length of the inspected pipeline.

• Kamburjan, Eduard; Din, Crystal Chang; Schlatte, Rudolf; Tarifa, Silvia Lizeth Tapia & Johnsen, Einar Broch (2022). Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 13701, p. 188–204. doi: 10.1007/978-3-031-19849-6_12. Full text in Research Archive Show summary

  Digital twin applications use digital artefacts to twin physical systems. The purpose is to continuously mirror the structure and behavior of the physical system, such that users can analyse the physical system by means of the digital twin. However, the physical system might change over time. In this case, the digital twin’s ensemble of digital artefacts needs to be reconfigured to correctly twin the physical system again. This paper considers a digital twin infrastructure combining MAPE-K feedback loops and semantic reflection to automatically ensure that the digital artefacts correctly twin the physical system; i.e., the resulting system is twinned-by-construction. We consider the monitoring of both structural and temporal correctness properties for digital twin, including the time delay required by reconfiguration, and the capture of execution traces to reflect digital threads in the digital twin framework.

• Kamburjan, Eduard; Klungre, Vidar Norstein; Schlatte, Rudolf; Tarifa, Silvia Lizeth Tapia; Cameron, David & Johnsen, Einar Broch (2022). Digital Twin Reconfiguration Using Asset Models. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 13704, p. 71–88. doi: 10.1007/978-3-031-19762-8_6. Full text in Research Archive
• Kobialka, Paul; Tarifa, Silvia Lizeth Tapia; Bergersen, Gunnar R. & Johnsen, Einar Broch (2022). Weighted Games for User Journeys. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 13550, p. 253–270. doi: 10.1007/978-3-031-17108-6_16. Full text in Research Archive
• Schlatte, Rudolf; Johnsen, Einar Broch; Kamburjan, Eduard & Tarifa, Silvia Lizeth Tapia (2022). The ABS simulator toolchain. Science of Computer Programming. ISSN 0167-6423. 223. doi: 10.1016/j.scico.2022.102861. Full text in Research Archive
• Päßler, Juliane; Aguado, Esther; Silva, Gustavo Rezende; Tarifa, Silvia Lizeth Tapia; Corbato, Carlos Hernández & Johnsen, Einar Broch (2022). A Formal Model of Metacontrol in Maude. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 13701, p. 575–596. doi: 10.1007/978-3-031-19849-6_32. Full text in Research Archive Show summary

  Nowadays smart applications appear in domains spanning from commodity household applications to advanced underwater robotics. These smart applications require adaptation to dynamic environments, changing requirements and internal system errors Metacontrol takes a systems of systems view on autonomous control systems and self-adaptation, by means of an additional layer of control that manipulates and combines the regular controllers. This paper develops a formal model of a Metacontrol architecture. We formalise this Metacontrol architecture in the context of an autonomous house heating application, enabling different controllers to be dynamically combined in order to meet user requirements to a better extent than the individual controllers in isolation. The formal model is developed in the Maude rewriting system, where we show results comparing different scenarios.

• Baramashetru, Chinmayi; Tarifa, Silvia Lizeth Tapia; Owe, Olaf & Gruschka, Nils (2022). A Policy Language to Capture Compliance of Data Protection Requirements. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 13274, p. 289–309. doi: 10.1007/978-3-031-07727-2_16. Full text in Research Archive Show summary

  From the very outset of the digital era, the protection of personal data against unauthorized usage and distribution has been one of the most significant challenges in distributed services. For this reason, new regulations such as the European Union’s the General Data Protection Regulation grant users tight control over their data that is handled by service providers. Compliance with such regulations can take expensive refitting of the existing systems and manual work. We propose a formal language that can define properties like informed consent, data subject rights, and the lawfulness to capture data protection requirements. The language is designed to abstract ownership information to make data dependencies explicit. We formalise a notion of policy compliance. This can be useful in service architecture with various actors who necessarily do not trust each other and may have conflicting interests.

• Tarifa, Silvia Lizeth Tapia (2022). Locally Abstract Globally Concrete Semantics of Time and Resource Aware Active Objects. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 13360, p. 481–499. doi: 10.1007/978-3-031-08166-8_23. Full text in Research Archive
• Schlatte, Rudolf; Johnsen, Einar Broch; Kamburjan, Eduard & Tarifa, Silvia Lizeth Tapia (2021). Modeling and Analyzing Resource-Sensitive Actors: A Tutorial Introduction. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. doi: 10.1007/978-3-030-78142-2_1. Full text in Research Archive
• Kamburjan, Eduard; Schlatte, Rudolf; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2021). Designing Distributed Control with Hybrid Active Objects. In Margaria, Tiziana & Steffen, Bernhard (Ed.), Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part IV. Springer. ISSN 9783030837228. p. 88–108. doi: 10.1007/978-3-030-83723-5_7. Full text in Research Archive
• Halvorsrud, Ragnhild; Mannhardt, Felix; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2021). Smart Journey Mining for Improved Service Quality. In Barbara, Carminati (Eds.), IEEE International Conference on Services Computing, SCC 2021. IEEE (Institute of Electrical and Electronics Engineers). ISSN 9781665416832. p. 367–369. doi: 10.1109/SCC53864.2021.00051. Full text in Research Archive Show summary

  This paper describes emergent challenges in extending and uniting research in service science and process mining. By combining formal representations of user journeys with process mining constructs, we aim to develop tools for automated capture and analysis of user interactions extending across service systems. Based on the resulting database of actual user journeys and user models, we will use logic-based techniques and machine learning to expose deviations and predict possible behaviours for pre-emptive problem solving and service recovery.

• Boer, Frank de; Bonsangue, Marcello; Johnsen, Einar Broch; Pun, Ka I; Tarifa, Silvia Lizeth Tapia & Tveito, Lars (2020). SymPaths: Symbolic Execution Meets Partial Order Reduction. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 12345, p. 313–338. doi: 10.1007/978-3-030-64354-6_13. Full text in Research Archive Show summary

  Symbolic execution is an important technique for software analysis, which enables systematic model exploration by following all possible execution paths for a given program. For multithreaded shared variable programs, this technique leads to a state space explosion. Partial order reduction is a technique which allows equivalent execution paths to be recognized, reducing the state space explosion problem. This paper provides formal justifications for these techniques in a multithreaded setting by proving the correctness and completeness of symbolic execution for multithreaded shared variable programs, with and without the use of partial order reduction. We then show how these formal justifications carry over to prove the soundness and relative completeness of a proof system for such multithreaded shared variable programs in dynamic logic, such that partial order reduction can be used to simplify the proof construction by mitigating the state space explosion.

• Boer, Frank de; Johnsen, Einar Broch; Pun, Ka I & Tarifa, Silvia Lizeth Tapia (2020). From SOS to asynchronously communicating actors. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 12226, p. 269–275. doi: 10.1007/978-3-030-57506-9_20. Full text in Research Archive Show summary

  Structural Operational Semantics (SOS) provides a general format to describe a model as a transition system with very powerful synchronization mechanisms. Actor systems are distributed, asynchronously communicating units of computation with encapsulated state, with much weaker means of synchronizing between actors. In this paper, we discuss an implementation of a SOS model using actors in the object-oriented actor language ABS and how to argue that global properties about the model are inherited from the SOS level to the actor implementation. The work stems from a case study modelling the memory system of a cache-coherent multicore architecture.

• Boer, Frank de; Johnsen, Einar Broch; Schlatte, Rudolf; Tarifa, Silvia Lizeth Tapia & Tveito, Lars (2020). Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages. OpenAccess Series in Informatics. 86, p. 10:1–10:18. doi: 10.4230/OASIcs.Gabbrielli.10. Full text in Research Archive Show summary

  This paper presents a method for testing whether objects in actor languages and active object languages exhibit locally deterministic behavior. We investigate such a method for a class of guarded command programs, abstracting from object-oriented features like method calls but focusing on cooperative scheduling of dynamically spawned processes executing in parallel. The proposed method can answer questions such as whether all permutations of an execution trace are equivalent, by generating candidate traces for testing which may lead to different final states. To prune the set of candidate traces, we employ partial order reduction. To further reduce the set, we introduce an analysis technique to decide whether a generated trace is schedulable. Schedulability cannot be decided for guarded commands using standard dependence and interference relations because guard enabledness is non-monotonic. To solve this problem, we use concolic execution to produce linearized symbolic traces of the executed program, which allows a weakest precondition computation to decide on the satisfiability of guards.

• Turin, Gianluca; Borgarelli, Andrea; Donetti, Simone; Johnsen, Einar Broch; Tarifa, Silvia Lizeth Tapia & Damiani, Ferruccio (2020). A Formal Model of the Kubernetes Container Framework. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 12476, p. 558–577. doi: 10.1007/978-3-030-61362-4_32. Full text in Research Archive Show summary

  Loosely-coupled distributed systems organized as collections of so-called cloud-native microservices are able to adapt to traffic in very fine-grained and flexible ways. For this purpose, the cloud-native microservices exploit containerization and container management systems such as Kubernetes. This paper presents a formal model of resource consumption and scaling for containerized microservices deployed and managed by Kubernetes. Our aim is that the model, developed in Real-Time ABS, can be used as a framework to explore the behavior of deployed systems under various configurations at design time—before the systems are actually deployed. We further present initial results comparing the observed behavior of instances of our modeling framework to corresponding observations of real systems. These preliminary results suggest that the modeling framework can provide a satisfactory accuracy with respect to the behavior of distributed microservices managed by Kubernetes.

• Bijo, Shiji; Johnsen, Einar Broch; Pun, Ka I & Tarifa, Silvia Lizeth Tapia (2019). A formal model of data access for multicore architectures with multilevel caches. Science of Computer Programming. ISSN 0167-6423. 179, p. 24–53. doi: 10.1016/j.scico.2019.04.003. Full text in Research Archive
• Bezirgiannis, Nikolaos; Boer, Frank de; Johnsen, Einar Broch; Pun, Ka I & Tarifa, Silvia Lizeth Tapia (2019). Implementing SOS with Active Objects: A Case Study of a Multicore Memory System. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 11424, p. 332–350. doi: 10.1007/978-3-030-16722-6_20. Full text in Research Archive Show summary

  This paper describes the development of a parallel simulator of a multicore memory system from a model formalized as a structural operational semantics (SOS). Our implementation uses the Abstract Behavioral Specification (ABS) language, an executable, active object modelling language with a formal semantics, targeting distributed systems. We develop general design patterns in ABS for implementing SOS, and describe their application to the SOS model of multicore memory systems. We show how these patterns allow a formal correctness proof that the implementation simulates the formal operational model and discuss further parallelization and fairness of the simulator.

• Mauro, Jacopo; Tarifa, Silvia Lizeth Tapia & Yu, Ingrid Chieh (2018). Automatic Parameter Optimisation of Service Quality and Resource Usage. NIKT: Norsk IKT-konferanse for forskning og utdanning. ISSN 1892-0713. Full text in Research Archive Show summary

  https://ojs.bibsys.no/index.php/NIK/article/view/504/430

• Bijo, Shiji; Johnsen, Einar Broch; Pun, Ka I Violet; Seidl, Christoph & Tarifa, Silvia Lizeth Tapia (2018). Deployment by Construction for Multicore Architectures. In Margaria, Tiziana & Steffen, Bernhard (Ed.), Leveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018. Proceedings - Part I. Springer. ISSN 9783030034177. p. 448–465. doi: 10.1007/978-3-030-03418-4_26. Full text in Research Archive
• Schlatte, Rudolf; Johnsen, Einar Broch; Mauro, Jacopo; Tarifa, Silvia Lizeth Tapia & Yu, Ingrid Chieh (2018). Release the Beasts: When Formal Methods Meet Real World Data. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 10865, p. 107–121. doi: 10.1007/978-3-319-90089-6_8. Full text in Research Archive
• Johnsen, Einar Broch; Pun, Ka I & Tarifa, Silvia Lizeth Tapia (2017). A formal model of cloud-deployed software and its application to workflow processing. In Begušić, Dinko; Rožić, Nikola; Radić, Joško & Šarić, Matko (Ed.), SoftCOM 2017. IEEE Sarnoff Symposium. ISSN 9789532900781. doi: 10.23919/SOFTCOM.2017.8115501. Full text in Research Archive
• Din, Crystal Chang; Hahnle, Reiner; Johnsen, Einar Broch; Pun, Ka I & Tarifa, Silvia Lizeth Tapia (2017). Locally abstract, globally concrete semantics of concurrent programming languages. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 10501 LNAI, p. 22–43. doi: 10.1007/978-3-319-66902-1_2. Full text in Research Archive
• Bijo, Shiji; Johnsen, Einar Broch; Pun, Ka I & Tarifa, Silvia Lizeth Tapia (2017). A formal model of parallel execution on multicore architectures with multilevel caches. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 10487 LNCS, p. 58–77. doi: 10.1007/978-3-319-68034-7_4. Full text in Research Archive
• Johnsen, Einar Broch; Pun, Ka I & Tarifa, Silvia Lizeth Tapia (2016). Modeling deployment decisions for elastic services with ABS. Electronic Proceedings in Theoretical Computer Science (EPTCS). 228, p. 16–26. doi: 10.4204/EPTCS.228.3. Full text in Research Archive
• Bijo, Shiji; Johnsen, Einar Broch; Pun, Ka I & Tarifa, Silvia Lizeth Tapia (2016). A Maude Framework for Cache Coherent Multicore Architectures. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 9942, p. 47–63. doi: 10.1007/978-3-319-44802-2_3. Full text in Research Archive
• Bijo, Shiji; Johnsen, Einar Broch; Pun, Ka I & Tarifa, Silvia Lizeth Tapia (2016). An operational semantics of cache coherent multicore architectures. In Ossowski, Sascha (Eds.), Proceedings of the 31st Annual ACM Symposium on Applied Computing (SAC '16). Association for Computing Machinery (ACM). ISSN 9781450337397. p. 1219–1224. doi: 10.1145/2851613.2851718. Full text in Research Archive
• Johnsen, Einar Broch; Pun, Ka I; Steffen, Martin; Tarifa, Silvia Lizeth Tapia & Yu, Ingrid Chieh (2016). Meeting Deadlines, Elastically. In Petre, Luigia & Sekerinski, Emil (Ed.), From Action Systems to Distributed Systems: The Refinement Approach. CRC Press. ISSN 9781498701587. p. 99–111. doi: 10.1201/b20053-11. Full text in Research Archive
• Din, Crystal Chang; Tarifa, Silvia Lizeth Tapia; Hähnle, Reiner & Johnsen, Einar Broch (2015). History-Based Specification and Verification of Scalable Concurrent and Distributed Systems. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 9407, p. 217–233. doi: 10.1007/978-3-319-25423-4_14. Full text in Research Archive
• Johnsen, Einar Broch; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2015). Integrating deployment architectures and resource consumption in timed object-oriented models. Journal of Logical and Algebraic Methods in Programming. ISSN 2352-2208. 84(1), p. 67–91. doi: 10.1016/j.jlamp.2014.07.001. Full text in Research Archive
• Brandauer, Stephan; Castegren, Elias; Clarke, Dave; Fernandez-Reyes, Kiko; Johnsen, Einar Broch & Pun, Ka I [Show all 9 contributors for this article] (2015). Parallel objects for multicores: A glimpse at the parallel language encore. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 9104, p. 1–56. doi: 10.1007/978-3-319-18941-3_1. Full text in Research Archive
• Johnsen, Einar Broch; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2014). Deployment variability in delta-oriented models. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 8802, p. 304–319. doi: 10.1007/978-3-662-45234-9_22. Full text in Research Archive
• Albert, Elvira; Boer, Frank de; Hähnle, Reiner; Johnsen, Einar Broch; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia [Show all 7 contributors for this article] (2014). Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS. Service Oriented Computing and Applications. ISSN 1863-2386. 8(4), p. 323–339. doi: 10.1007/s11761-013-0148-0. Full text in Research Archive
• Johnsen, Einar Broch; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2013). Modeling Application-Level Management of Virtualized Resources in ABS. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7542, p. 89–108. doi: 10.1007/978-3-642-35887-6_5. Full text in Research Archive
• Bjørk, Joakim; Boer, Frank de; Johnsen, Einar Broch; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2012). User-defined Schedulers for Real-Time Concurrent Objects. Innovations in Systems and Software Engineering. ISSN 1614-5046. doi: 10.1007/s11334-012-0184-5. Full text in Research Archive
• Johnsen, Einar Broch; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2012). A Formal Model of Object Mobility in Resource-Restricted Deployment Scenarios. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7253, p. 187–204. doi: 10.1007/978-3-642-35743-5_12. Full text in Research Archive
• Johnsen, Einar Broch; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2012). A Formal Model of User-Defined Resources in Resource-Restricted Deployment Scenarios. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7421, p. 196–213. doi: 10.1007/978-3-642-31762-0_13. Full text in Research Archive
• Johnsen, Einar Broch; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2012). Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7635, p. 71–86. doi: 10.1007/978-3-642-34281-3_8. Full text in Research Archive
• Johnsen, Einar Broch; Owe, Olaf; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2011). Validating Timed Models of Deployment Components with Parametric Concurrency. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6528, p. 46–60. doi: 10.1007/978-3-642-18070-5_4. Full text in Research Archive
• Johnsen, Einar Broch; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2011). Integrating Aspects of Software Deployment in High-Level Executable Models, Norsk Informatikkonferanse NIK 2011. Tapir Akademisk Forlag. ISSN 9788251928434. Full text in Research Archive
• Albert, Elvira; Genaim, Samir; Gómez-Zamalloa, Miguel; Johnsen, Einar Broch; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2011). Simulating Concurrent Behaviors with Worst-Case Cost Bounds. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6664, p. 353–368. doi: 10.1007/978-3-642-21437-0_27. Full text in Research Archive
• Schlatte, Rudolf; Johnsen, Einar Broch; Kazemeyni, Fatemeh Sadat & Tarifa, Silvia Lizeth Tapia (2011). Models of Rate Restricted Communication for Concurrent Objects. Electronical Notes in Theoretical Computer Science. 274, p. 67–81. doi: 10.1016/j.entcs.2011.07.007. Full text in Research Archive
• Johnsen, Einar Broch; Owe, Olaf; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2010). Dynamic Resource Reallocation between Deployment Components. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6447, p. 646–661. Full text in Research Archive
• Johnsen, Einar Broch; Owe, Olaf; Schlatte, Rudolf & Tarifa, Silvia Lizeth Tapia (2010). Deployment Components with Parametric Concurrency. In Walden, Marina & Petre, Luigia (Ed.), Proceedings of the 22nd Nordic Workshop on Programming Theory, NWPT'10. TUCS. ISSN 9789521224782. p. 23–25. Full text in Research Archive

View all works in NVA

• Abraham, Erika; Clemens, Dubslaff & Tarifa, Silvia Lizeth Tapia (2023). Proceedings of the 20th International Colloquium on Theoretical Aspects of Computing - ICTAC 2023. Springer. ISBN 9783031479625. 440 p. Full text in Research Archive
• Tarifa, Silvia Lizeth Tapia & Proença, José (2022). Formal Aspects of Component Software. 18th International Conference, FACS 2022, Virtual Event, November 10–11, 2022, Proceedings. Springer. ISBN 9783031208713. 245 p. Full text in Research Archive
• Ahrendt, Wolfgang & Tarifa, Silvia Lizeth Tapia (2019). Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings. Springer. ISBN 9783030349677. 551 p. Full text in Research Archive

View all works in NVA

• Pässler, Juliane Linda; Beek, Maurice H. ter; Damiani, Ferruccio; Dubslaff, Clemens; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2025). Feature-Oriented Modelling and Analysis of a Self-Adaptive Robotic System. Association for Computing Machinery (ACM). A, p. 238–238. doi: 10.1145/3744915.3748484. Full text in Research Archive
• Tarifa, Silvia Lizeth Tapia; Proença, José & Oliveira, Jose (2025). Introduction to the Special Collection from FACS 2022. Formal Aspects of Computing. ISSN 0934-5043. 37(2). doi: 10.1145/3703357. Full text in Research Archive
• Kobialka, Paul; Pferscher, Andrea; Bergersen, Gunnar Rye; Tarifa, Silvia Lizeth Tapia & Johnsen, Einar Broch (2024). Stochastic Games for User Journeys. Full text in Research Archive
• Kobialka, Paul; Schlatte, Rudolf; Bergersen, Gunnar Rye; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2023). Simulating User Journeys with Active Objects. Full text in Research Archive
• Kobialka, Paul; Bergersen, Gunnar Rye; Tarifa, Silvia Lizeth Tapia & Johnsen, Einar Broch (2022). Weighted Games for User Journeys. Full text in Research Archive
• Kobialka, Paul; Mannhardt, Felix; Tarifa, Silvia Lizeth Tapia & Johnsen, Einar Broch (2022). Building User Journey Games from Multi-party Event Logs. Full text in Research Archive
• Ahrendt, Wolfgang; Tarifa, Silvia Lizeth Tapia & Wehrheim, Heike (2021). Formal Aspects of Computing, Volume 33, Number 6, December 2021. Extended versions of papers presented at iFM 2019. Formal Aspects of Computing. ISSN 0934-5043. 33(6). doi: 10.1007/s00165-021-00569-w. Full text in Research Archive
• Halvorsrud, Ragnhild; Mannhardt, Felix; Johnsen, Einar Broch & Tarifa, Silvia Lizeth Tapia (2021). Smart Journey Mining for Improved Service Quality. Full text in Research Archive Show summary

  This paper describes emergent challenges in extending and uniting research in service science and process mining. By combining formal representations of user journeys with process mining constructs, we aim to develop tools for automated capture and analysis of user interactions extending across service systems. Based on the resulting database of actual user journeys and user models, we will use logic-based techniques and machine learning to expose deviations and predict possible behaviours for pre-emptive problem solving and service recovery.

• Borda, Aimée; Cimini, Matteo; Cirstea, Corina; Dardha, Ornela; Fowler, Simon & ć, Svetlana Jakši [Show all 19 contributors for this article] (2019). Preface. Electronic Proceedings in Theoretical Computer Science (EPTCS). 304. Full text in Research Archive
• Pässler, Juliane Linda; Tarifa, Silvia Lizeth Tapia; Corbato, Carlos Hernandez & Johnsen, Einar Broch (2025). Formal Methods for Self-Adaptive Systems. Universitetet i Oslo. Full text in Research Archive Show summary

  Self-adaptation can be used to enable a system to adapt to internal and external changes, allowing it to be deployed in an uncertain environment. A selfadaptive system (SAS) can be implemented as a two-layered system consisting of a managed subsystem and a managing subsystem. The managed subsystem implements the application logic, while the managing subsystem implements the adaptation logic. The managing subsystem monitors the managed subsystem and the environment, uses this data to determine whether the managed subsystem needs to be adapted, and adapts it if necessary. The aim of an SAS is to perform its mission autonomously, ideally without human supervision. Especially when operating in safety and security-critical domains, it is crucial to ensure the safety and reliability of an SAS. In this thesis, we show how formal methods can be used to analyse the safety and reliability of SASs. Formal methods are mathematically based techniques and tools for the specification and analysis of hardware and software systems. We focus on formal methods that are able to capture and analyse the two-layered structure of an SAS, including the interaction between the two layers and the influence of the environment that triggers self-adaptation of the SAS. Concretely, we show how rewriting logic and techniques from software product lines (SPLs) can be used to model an SAS and the environment it operates in. We exemplify the former using the tool Maude and the latter with the tool ProFeat. We use simulation in Maude to show that the inclusion of a managing subsystem, which implements self-adaptation, can increase the overall system performance. Family-based probabilistic model checking in ProFeat is utilised to illustrate how quantitative properties of an SAS can be analysed. We further show how existing formal modelling techniques can be extended or modified to support reuse of SAS models, and show their potential to ease modelling and maintenance of SASs. By introducing template nodes in decision diagrams, common behaviour can be encapsulated and reused which also supports the specification of the two-layered structure of an SAS. Furthermore, we combine the modelling of the structure and the behaviour of SPLs into one compositional model, called behavioural feature model, which allows reuse of behaviour of single features and sets of features.

• Baramashetru, Chinmayi; Tarifa, Silvia Lizeth Tapia; Gruschka, Nils & Owe, Olaf (2025). Data Privacy Compliance by Construction in Distributed Systems. GDPR Enforcement, Privacy by Design and Consent-Based Data Handling. Universitetet i Oslo. Full text in Research Archive Show summary

  As digital systems increasingly rely on the collection and processing of personal data, it becomes difficult to ensure balance between data processing and user’s privacy. In response to increasing data mishandling and complex regulatory landscapes, the European Union enacted the General Data Protection Regulation (GDPR) to enforce structured and transparent handling of personal data. It introduces strict obligations for data privacy by design and default, consent based processing, and purpose limitation, yet its legal abstraction offers little guidance for technical implementation. This thesis investigates how data protection requirements, especially those mentioned in the GDPR can be formally modeled and enforced through programming language techniques. It develops a sequence of language-based techniques to offer data privacy compliance by construction in distributed, actor-based systems, with user consent and purpose based processing at its core. The first contribution proposes a policy specification language that concisely expresses data privacy requirements, usage restrictions, and captures consent. It is designed as a high-level, declarative abstraction for capturing users’ privacy preferences and systematically aligning them with GDPR principles within Distributed systems. It expresses the notion of policy compliance for a distributed system with multiple actors with conflicting policies. Furthermore, it uses a taxonomy-based expression for policy filtering and supports granular policy specification. To bridge the gap between policy level reasoning and programming Language support, the thesis next presents a privacy-aware active object language (PAOL) that integrates GDPR concepts such as consent, purpose limitation, personal data, and data privacy compliance as programming language constructs in its syntax and semantics. It ensures that operations on personal data are checked at runtime and each step or operation is supported by valid, current consent. This runtime enforcement is next complemented by a type system for enforcing GDPR-aligned behavior statically. TyPAOL extends the PAOL by incorporating a type and constraint inference system to enforce GDPR based data privacy policies. It adopts a hybrid type checking mechanism that shifts compliance checks from execution to method activation. This approach ensures that no method execution proceeds unless all the generated type constraints are satisfied at method activation, thereby avoiding mid-execution failures. It provides a formal proof of soundness and ensures data privacy compliance for a running object within a well typed-configuration. In order to validate our programs, a rewriting logic based framework i.e., Maude, is used to develop a proof of concept of the proposed framework.

• Baramashetru, Chinmayi; Tarifa, Silvia Lizeth Tapia & Owe, Olaf (2023). Integrating Data Privacy Compliance in Active Object Languages. Universitetet i Oslo. ISSN 9788273686060. Full text in Research Archive Show summary

  As users are more and more required to share their personal data, it becomes increasingly important for applications to comply with users’ consent for the handling of their personal data. Ensuring compliance with such consent requires reasoning globally about both the flow of information and the interaction of different parties handling personal data. In this direction, privacy by design principles cultivate a philosophy that endorses the development of systems with built-in abilities to demonstrate compliance with data privacy to guarantee the protection of personal data. However, there is an apparent mismatch in adopting such imprecise principles into explicit methods that support systematic solutions that integrates data privacy in system design. In this paper, we propose an integration of privacy concepts into a core active object language, to explore how the chosen language semantics can ensure personal data handling according to users’ privacy consent.

• Abraham, Erika & Tarifa, Silvia Lizeth Tapia (2018). Proceedings of the PhD Symposium at iFM’18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM’18). Universitetet i Oslo. ISSN 9788273684356. Full text in Research Archive
• Abraham, Erika; Tarifa, Silvia Lizeth Tapia & Abraham, Erika (2017). Proceedings of the PhD Symposium at iFM’17 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM’17). Universitetet i Oslo. ISSN 9788273684356. Full text in Research Archive
• Bijo, Shiji; Johnsen, Einar Broch; Pun, Ka I & Tarifa, Silvia Lizeth Tapia (2015). An Operational Semantics of Cache Coherent Multicore Architectures. Universitetet i Oslo. Full text in Research Archive
• Johnsen, Einar Broch; Pun, Ka I; Steffen, Martin; Tarifa, Silvia Lizeth Tapia & Yu, Ingrid Chieh (2015). Meeting Deadlines, Elastically. Universitetet i Oslo. ISSN 9788273684080. Full text in Research Archive
• Tarifa, Silvia Lizeth Tapia (2014). Executable Modeling of Deployment Decisions for Resource-Aware Distributed Applications. Universitetet i Oslo. Full text in Research Archive Show summary

  The increasing popularity of virtualized services and cloud computing, offering elastic and scalable computing resources challenges software engineering methods by asking a number of new questions: How can we integrate deployment-specific information in the overall design of software applications? How can we express and compare deployment decisions in the design phase, so that performance diagnosis can happen early in the software development cycle? How do we design scalable applications? This thesis proposes a methodology for the modeling and analysis of object-oriented distributed applications that are able to adapt to changes in client traffic, so that they can keep desired levels of performance. As a starting point for developing our methodology, we take Core ABS, an abstract, behavioral specification language that targets the executable modeling of concurrent, distributed and object-oriented systems. We extend Core ABS with deployment-specific information such as deployment architectures, flexible application-specific schedulers, deadlines at the application level, resource management primitives, and user-defined resource costs. The extensions are developed following conventions of formal methods, combining rigorous definitions and formal semantics with a user-friendly Java-like syntax and tool support. By exploiting these language extensions, our methodology makes it possible to compare at the modeling level how a software behaves under different deployment choices. Such comparisons allow a better understanding of the trade-offs from different deployment choices, consequently better design decisions for distributed applications can be made early in the software development life cycle. By integrating resource management and deployment decisions in the design phase, our methodology has the potential to improve the software engineering process for virtualized and scalable software applications running in the cloud, both with respect to quality and with respect to development and deployment cost.

• Tarifa, Silvia Lizeth Tapia (2013). The Cooperative Cleaners Case Study: Modelling and Analysis in Real-Time ABS. Universitetet i Oslo. Full text in Research Archive Show summary

  Swarm robotics has been proposed as a way to organise decentralised systems in which a large number of similar robots, that are autonomous and relatively simple in their behaviour, are coordinated in a way that leads to an emergent useful behaviour. The Cooperative Cleaners case study is an example of swarm robotics. In this case study, a group of robots cooperate in order to reach the common goal of cleaning a dirty floor. A cleaning robot has a bounded amount of memory; it can only observe the state of the floor in its immediate surroundings and decide on its movement based on these observations. The cleaning robots use indirect communication based on sensing and signalling, and the desired goal of cleaning the whole floor is thus an emergent behaviour of the swarm. In this thesis we show how the Cooperative Cleaners case study can be modelled and analysed using the Real-Time ABS language. Real-Time ABS is a timed, abstract and behavioural specification language with a formal semantics and a Java-like syntax that targets concurrent, distributed and object- oriented systems. We use the features of Real-Time ABS in the development of our model of the Cooperative Cleaners problem in order to evaluate how well Real-Time ABS can be used to model and analyse the behaviour of systems from the swarm robotics domain. Our work shows that Real-Time ABS can facilitate the modelling of these kinds of systems, but due to the challenges introduced when formally modelling systems in this domain, it requires fairly advanced modelling skills to obtain an adequate model. However the analysis of these kinds of systems is currently restricted to simulations applied to small scenarios.

View all works in NVA