ADAPT (completed)

• 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.

• 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
• 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
• Lebesbye, Torgeir; Mauro, Jacopo; Turin, Gianluca & Yu, Ingrid Chieh (2021). Boreas – A Service Scheduler for Optimal Kubernetes Deployment. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. p. 221–237. doi: 10.1007/978-3-030-91431-8_14. Full text in Research Archive Show summary

  The advent of cloud computing radically changed the way organisations operate their applications and allows them to achieve high availability of services at affordable cost. Most cloud-computing platforms fostered Kubernetes for their container orchestration and service management. The scheduler is a key component of Kubernetes, as it is responsible for finding the placement of new service containers when they are deployed. The default scheduler is very fast, although often suboptimal. This can lead to inefficient placement of services, or more severely, inability to deploy. We present a custom Kubernetes scheduler, dubbed Boreas, which is designed to evaluate bursts of deployment requests concurrently. Boreas finds the optimal placements for service containers with their deployment constraints by utilising a configuration optimiser. Results show that Boreas is able to find placements where the default Kubernetes scheduler fails, wasting less computing resources, or proving that no feasible deployment solution is possible.

• 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; 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.

• 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.

• 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

View all works in NVA

• 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

• 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

View all works in NVA