Rudolf Schlatte

• Kamburjan, Eduard; Klungre, Vidar Norstein; Qu, Yuanwei; Schlatte, Rudolf; Kostylev, Egor V. & Giese, Martin [Show all 7 contributors for this article] (2026). Semantically Reflected Programs. Transactions on Graph Data and Knowledge (TGDK). 4(1), p. 3:1–3:52. doi: 10.4230/TGDK.4.1.3. Full text in Research Archive Show summary

  This paper addresses the dichotomy between the formalization of structural and the formalization of executable behavioral knowledge by means of semantically lifted programs, which explore an intuitive connection between imperative programs and knowledge graphs. While knowledge graphs and ontologies are eminently useful to represent formal knowledge about a system’s individuals and universals, programming languages are designed to describe the system’s evolution. To address this dichotomy, we introduce a semantic lifting of the program states of an executing progam into a knowledge graph, for an object-oriented programming language. The resulting graph is exposed as a semantic reflection layer within the programming language, allowing programmers to leverage knowledge of the application domain in their programs during execution. In this paper, we formalize semantic lifting and semantic reflection for a small imperative programming language, SMOL, explain the operational aspects of the language, and consider type correctness and virtualization for runtime program queries through the semantic reflection layer. We illustrate semantic lifting and semantic reflection through a case study of geological modeling and discuss different applications of the technique. The language implementation is open source and available online.

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

• Stenseth, Nils Christian; Schlatte, Rudolf; Liu, Xiaoli; Pielke, Roger Jr.; Chen, Ben & Bjørnstad, Ottar Nordal [Show all 13 contributors for this article] (2023). Reply to Ekström and Ottersen: Real-time access to data during outbreaks is a key to avoid a local epidemic becoming a global pandemic. Proceedings of the National Academy of Sciences of the United States of America (PNAS). ISSN 0027-8424. 120(40). doi: 10.1073/pnas.2312649120. Full text in Research Archive
• 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.

• Stenseth, Nils Christian; Schlatte, Rudolf; Liu, Xiaoli; Pielke, Roger; Li, Ruiyun & Chen, Bin [Show all 18 contributors for this article] (2023). How to avoid a local epidemic becoming a global pandemic. Proceedings of the National Academy of Sciences of the United States of America (PNAS). ISSN 0027-8424. 120(10). doi: 10.1073/pnas.2220080120. Full text in Research Archive Show summary

  Here, we combine international air travel passenger data with a standard epidemiological model of the initial 3 mo of the COVID-19 pandemic (January through March 2020; toward the end of which the entire world locked down). Using the information available during this initial phase of the pandemic, our model accurately describes the main features of the actual global development of the pandemic demonstrated by the high degree of coherence between the model and global data. The validated model allows for an exploration of alternative policy efficacies (reducing air travel and/or introducing different degrees of compulsory immigration quarantine upon arrival to a country) in delaying the global spread of SARS-CoV-2 and thus is suggestive of similar efficacy in anticipating the spread of future global disease outbreaks. We show that a lesson from the recent pandemic is that reducing air travel globally is more effective in reducing the global spread than adopting immigration quarantine. Reducing air travel out of a source country has the most important effect regarding the spreading of the disease to the rest of the world. Based upon our results, we propose a digital twin as a further developed tool to inform future pandemic decision-making to inform measures intended to control the spread of disease agents of potential future pandemics. We discuss the design criteria for such a digital twin model as well as the feasibility of obtaining access to the necessary online data on international air travel.

• Horn, Geir; Schlatte, Rudolf & Johnsen, Einar Broch (2022). Digital Twins for Autonomic Cloud Application Management. In Barolli, Leonard; Hussain, Farookh & Enokido, Tomoya (Ed.), Advanced Information Networking and Applications: Proceedings of the 36th International Conference on Advanced Information Networking and Applications (AINA-2022), Volume 3. Springer. ISSN 9783030996185. p. 141–152. doi: 10.1007/978-3-030-99619-2_14. Full text in Research Archive Show summary

  Cloud applications are distributed in nature, and it is challenging to orchestrate an application across different Cloud providers and for the different capabilities along the Cloud continuum, from the centralized data centers to the edge of the network. Furthermore, optimal dynamic reconfiguration of an application often takes more time than available at runtime. The approach presented in this paper uses a concurrent simulation model of the application that is continuously updated with real-time monitoring data, optimizing, and validating deployment reconfiguration decisions prior to enacting them for the running applications. This enables proactive decisions to be taken for a future time point, thereby allowing ample time for the reconfiguration actions, as well as realistic Bayesian estimation of the application’s time variate operational parameters for the optimization process.

• Schlatte, Rudolf (2022). A Note on Idleness Detection of Actor Systems. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 13360, p. 437–445. doi: 10.1007/978-3-031-08166-8_21. Full text in Research Archive Show summary

  In an actor system, detecting global idleness is trivial if the global state can be inspected synchronously. A distributed implementation, especially with asynchronous messages, poses more problems. This paper discusses detecting idleness in actor systems with various characteristics, among them topology and message passing semantics. We present a TLA+ specification of a simple termination detection algorithm, add necessary conditions missing in the original description, and establish a correctness invariant to model-check the specification against. We further show via model-checking that the algorithm only works with synchronous messages but is robust against message reordering. We then model and discuss a simplified version of the idleness detection implementation in the Erlang backend of the ABS modeling language.

• 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
• 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
• 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
• Tveito, Lars; Johnsen, Einar Broch & Schlatte, Rudolf (2020). Global Reproducibility Through Local Control for Distributed Active Objects. In Wehrheim, Heike & Cabot, Jordi (Ed.), Fundamental Approaches to Software Engineering 23rd International Conference, FASE 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings. Springer. ISSN 9783030452339. p. 140–160. doi: 10.1007/978-3-030-45234-6_7. Full text in Research Archive Show summary

  Non-determinism in a concurrent or distributed setting may lead to many different runs or executions of a program. This paper presents a method to reproduce a specific run for non-deterministic actor or active object systems. The method is based on recording traces of events reflecting local transitions at so-called stable states during execution; i.e., states in which local execution depends on interaction with the environment. The paper formalizes trace recording and replay for a basic active object language, to show that such local traces suffice to obtain global reproducibility of runs; during replay different objects may operate fairly independently of each other and in parallel, yet a program under replay has guaranteed deterministic outcome. We then show that the method extends to the other forms of non-determinism as found in richer active object languages. Following the proposed method, we have implemented a tool to record and replay runs, and to visualize the communication and scheduling decisions of a recorded run, for Real-Time ABS, a formally defined, rich active object language for modeling timed, resource-aware behavior in distributed systems.

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

• 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
• Din, Crystal Chang; Schlatte, Rudolf & Chen, Tzu-Chun (2018). Program Verification for Exception Handling on Active Objects Using Futures. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 10886, p. 73–88. doi: 10.1007/978-3-319-92970-5_5. Full text in Research Archive Show summary

  For implementing correct systems, handling and recovering from exceptional situations is important but challenging for ensuring correct interactions among distributed objects which are processing concurrently. To focus on exploring novel handling constructs for actor-based programming languages, we study ABS, an actor-based concurrent modeling language with an underlying executable formal semantics. This paper introduces multi-party session blocks with recovery handlers for exceptions into ABS. With this novel construct, we verify the correctness of interactions among objects within a session block. Program correctness is ensured by specifying invariants as pre- and post-conditions, called session contracts, for such a block, which is more expressive than the existing class invariant proof system for ABS. We present the extension of ABS with a try-catch-finally construct and class session recovery blocks that handle uncaught exceptions.

• Soylu, Ahmet; Giese, Martin; Schlatte, Rudolf; Jimenez-Ruiz, Ernesto; Kharlamov, Evgeny & Özçep, Özgür [Show all 8 contributors for this article] (2017). Querying industrial stream-temporal data: An ontology-based visual approach. Journal of Ambient Intelligence and Smart Environments. ISSN 1876-1364. 9(1), p. 77–95. doi: 10.3233/AIS-160415. Full text in Research Archive Show summary

  An increasing number of sensors are being deployed in business-critical environments, systems, and equipment; and stream a vast amount of data. The operational efficiency and effectiveness of business processes rely on domain experts’ agility in interpreting data into actionable business information. A domain expert has extensive domain knowledge but not necessarily skills and knowledge on databases and formal query languages. Therefore, centralised approaches are often preferred. These require IT experts to translate the information needs of domain experts into extract-transform-load (ETL) processes in order to extract and integrate data and then let domain experts apply predefined analytics. Since such a workflow is too time intensive, heavy-weight and inflexible given the high volume and velocity of data, domain experts need to extract and analyse the data of interest directly. Ontologies, i.e., semantically rich conceptual domain models, present an intelligible solution by describing the domain of interest on a higher level of abstraction closer to the reality. Moreover, recent ontology-based data access (OBDA) technologies enable end users to formulate their information needs into queries using a set of terms defined in an ontology. Ontological queries could then be translated into SQL or some other database query languages, and executed over the data in its original place and format automatically. To this end, this article reports an ontology-based visual query system (VQS), namely OptiqueVQS, how it is extended for a stream-temporal query language called STARQL, a user experiment with the domain experts at Siemens AG, and STARQL’s query answering performance over a proof of concept implementation for PostgreSQL.

• Soylu, Ahmet; Kharlamov, Evgeny; Zheleznyakov, Dmitriy; Jimenez-Ruiz, Ernesto; Giese, Martin & Skjæveland, Martin G [Show all 11 contributors for this article] (2017). OptiqueVQS: a Visual Query System over Ontologies for Industry. Semantic Web – Interoperability, Usability, Applicability. ISSN 1570-0844. p. 1–28. doi: 10.3233/sw-180293. Full text in Research Archive Show summary

  An important application of semantic technologies in industry has been the formalisation of information models using OWL~2 ontologies and the use of RDF for storing and exchanging application data. Moreover, legacy data can be virtualised as RDF using ontologies following the ontology-based data access (OBDA) approach. In all these applications, it is important to provide domain experts with query formulation tools for expressing their information needs in terms of queries over ontologies. In this work, we present such a tool, OptiqueVQS, which is designed based on our experience with OBDA applications in Statoil and Siemens and on best HCI practices for interdisciplinary engineering environments. OptiqueVQS implements a number of unique techniques distinguishing it from analogous query formulation systems. In particular, it exploits ontology projection techniques to enable graph-based navigation over an ontology during query construction. Secondly, while OptiqueVQS is primarily ontology driven, it exploits sampled data to enhance selection of data values for some data attributes. Finally, OptiqueVQS is built on well grounded requirements, design rationale, and quality attributes. We evaluated OptiqueVQS with both domain experts and casual users and qualitatively compared our system against prominent visual systems for ontology-driven query formulation and exploration of semantic data. OptiqueVQS is available online and can be downloaded together with an example OBDA scenario.

• Domenech, Jesus; Genaim, Samir; Johnsen, Einar Broch & Schlatte, Rudolf (2017). EASYINTERFACE: A toolkit for rapid development of GUIs for research prototype tools. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 10202 LNCS, p. 379–383. doi: 10.1007/978-3-662-54494-5_22. Full text in Research Archive
• Soylu, Ahmet; Giese, Martin; Schlatte, Rudolf; Jiménez-Ruiz, Ernesto; Ozcep, Ozgur & Brandt, Sebastian (2016). Domain experts surfing on stream sensor data over ontologies. CEUR Workshop Proceedings. 1588, p. 11–20. Full text in Research Archive
• Soylu, Ahmet; Giese, Martin; Jimenez-Ruiz, Ernesto; Kharlamov, Evgeny; Schlatte, Rudolf & Neuenstadt, Christian [Show all 11 contributors for this article] (2016). Ontology-based visual querying with OptiqueVQS: Statoil and Siemens cases. CEUR Workshop Proceedings. 1818, p. 34–39. Full text in Research Archive
• Soylu, Ahmet; Giese, Martin; Schlatte, Rudolf; Jiménez-Ruiz, Ernesto; Özcep, Özgür & Brandt, Sebastian (2016). A visual query system for stream data access over ontologies. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 9989, p. 161–166. doi: 10.1007/978-3-319-47602-5_32. 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
• Lanese, Ivan; Lienhardt, Michael; Bravetti, Mario; Johnsen, Einar Broch; Schlatte, Rudolf & Stolz, Volker [Show all 7 contributors for this article] (2014). Fault Model Design Space for Cooperative Concurrency. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 8803(2), p. 22–36. doi: 10.1007/978-3-662-45231-8_3. Full text in Research Archive
• Göri, Georg; Johnsen, Einar Broch; Schlatte, Rudolf & Stolz, Volker (2014). Erlang-style error recovery for concurrent objects with cooperative scheduling. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 8803(2), p. 5–21. doi: 10.1007/978-3-662-45231-8_2. 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
• Giese, Martin; Calvanese, Diego; Haase, Peter; Horrocks, Ian; Ioannidis, Yannis & Kllapi, Herald [Show all 16 contributors for this article] (2013). Scalable End-user Access to Big Data. In Akerkar, Rajendra (Eds.), Big Data Computing. Taylor & Francis. ISSN 9781466578371. doi: 10.1201/b16014-9. 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
• Kharlamov, Evgeny; Jimenez-ruiz, Ernesto; Zheleznyakov, Dmitriy; Bilidas, Dimitris; Giese, Martin & Haase, Peter [Show all 16 contributors for this article] (2013). Optique: Towards OBDA Systems for Industry. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7955, p. 125–140. doi: 10.1007/978-3-642-41242-4_11. 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
• Wong, Peter Y. H.; Albert, Elvira; Muschevici, Radu; Proenca, Jose; Schäfer, Jan & Schlatte, Rudolf (2012). The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. International Journal on Software Tools for Technology Transfer (STTT). ISSN 1433-2779. 14(5), p. 567–588. doi: 10.1007/s10009-012-0250-1. Full text in Research Archive Show summary

  Modern software systems must support a high degree of variability to accommodate a wide range of requirements and operating conditions. This paper introduces the Abstract Behavioural Specification (ABS) language and tool suite, a comprehensive platform for developing and analysing highly adaptable distributed concurrent software systems. The ABS language has a hybrid functional and object- oriented core, and comes with extensions that support the development of systems that are adaptable to diversified requirements, yet capable to maintain a high level of trustworthiness. Using ABS, system variability is consistently traceable from the level of requirements engineering down to object behaviour. This facilitates temporal evolution, as changes to the required set of features of a system are automatically reflected by functional adaptation of the system’s behaviour. The analysis capabilities of ABS stretch from debugging, observing and simulating to resource analysis of ABS models and help ensure that a system will remain dependable throughout its evolutionary lifetime. We report on the experience of using the ABS language and the ABS tool suite in an industrial case study.

• Nobakht, Behrooz; Boer, Frank S. de; Jaghoori, Mohammad Mahdi & Schlatte, Rudolf (2012). Programming and deployment of active objects with application-level scheduling. In Ossowski, Sascha & Lecca, Paola (Ed.), Proceedings of the 27th Annual ACM Symposium on Applied Computing. Association for Computing Machinery (ACM). ISSN 9781450308571. p. 1883–1888. doi: 10.1145/2245276.2232086. Full text in Research Archive Show summary

  We extend and implement a modeling language based on concurrent active objects with application-level scheduling policies. The language allows a programmer to assign priorities at the application level, for example, to method definitions and method invocations, and assign corresponding policies to the individual active objects for scheduling the messages. Thus, we leverage scheduling and performance related issues, which are becoming increasingly important in multi-core and cloud applications, from the underlying operating system to the application level. We describe a tool-set to transform models of active objects extended with application-level scheduling policies into Java. This tool-set allows a direct use of Java class libraries; thus, we obtain a full-fledged programming language based on active objects which allows for high-level control of deployment related issues.

• 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
• Boer, Frank de; Hähnle, Reiner; Johnsen, Einar Broch; Schlatte, Rudolf & Wong, Peter Y. H. (2012). Formal Modeling of Resource Management for Cloud Architectures: An Industrial Case Study. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7592, p. 91–106. doi: 10.1007/978-3-642-33427-6_7. Full text in Research Archive
• Leister, Wolfgang; Bjørk, Joakim; Schlatte, Rudolf; Johnsen, Einar Broch & Griesmayer, Andreas (2012). Exploiting Model Variability in ABS to Verify Distributed Algorithms. International Journal On Advances in Telecommunications. 5(1&2), p. 55–68. Full text in Research Archive Show summary

  We show a way to evaluate functional properties of distributed algorithms by the example of the AODV algorithm in sensor networks, Creol and ABS models, and component testing. We present a new method to structure the evaluation work into the categories of techniques, perspectives, arrangements, and properties using executable models. We demonstrate how to use this structure for network simulations and component testing using Creol models and demonstrate how the delta modelling technique of the ABS language can be used to facilitate the approach.

• Johnsen, Einar Broch; Hähnle, Reiner; Schäfer, Jan; Schlatte, Rudolf & Steffen, Martin (2011). ABS: A Core Language for Abstract Behavioral Specification. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6957. doi: 10.1007/978-3-642-25271-6_8. Full text in Research Archive
• Clarke, Dave; Muschevici, Radu; Proenca, Jose; Schaefer, Ina & Schlatte, Rudolf (2011). Variability Modelling in the ABS Language. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6957, p. 204–224. doi: 10.1007/978-3-642-25271-6_11. Full text in Research Archive Show summary

  The HATS project aims at developing a model-centric methodology for the design, implementation and verification of highly configurable systems, such as software product lines, centred around the Abstract Behavioural Specification (ABS) modelling Language. This article describes the variability modelling features of the ABS Modelling framework. It consists of four languages, namely, μTVL for describing feature models at a high level of abstraction, the Delta Modelling Language DML for describing variability of the ‘code’ base in terms of delta modules, the Product Line Configuration Language CL for linking feature models and delta modules together and the Product Selection Language PSL for describing a specific product to extract from a product line. Both formal semantics and examples of each language are presented.

• 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
• Clarke, Dave; Diakov, Nikolay; Hähnle, Reiner; Johnsen, Einar Broch; Schaefer, Ina & Schäfer, Jan [Show all 8 contributors for this article] (2011). Modeling Spatial and Temporal Variability with the HATS Abstract Behavioral Modeling Language. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6659, p. 417–457. doi: 10.1007/978-3-642-21455-4_13. Full text in Research Archive
• Leister, Wolfgang; Bjørk, Joakim; Schlatte, Rudolf & Griesmayer, Andreas (2011). Verifying Distributed Algorithms with Executable Creol Models, PESARO 2011 The First International Conference on Performance, Safety and Robustness in Complex Systems and Applications, April 17-22, 2011, Budapest, Hungary. International Academy, Research and Industry Association (IARIA). ISSN 9781612080055. 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
• Grabe, Immo; Jaghoori, Mohammad Mahdi; Klein, Joachim; Klüppelholz, Sascha; Stam, Andries & Baier, Christel [Show all 18 contributors for this article] (2010). The Credo Methodology (Extended Version). Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6286, p. 41–69. Full text in Research Archive
• Bjørk, Joakim; Johnsen, Einar Broch; Owe, Olaf & Schlatte, Rudolf (2010). Lightweight Time Modeling in Timed Creol. Electronic Proceedings in Theoretical Computer Science (EPTCS). 36, p. 67–81. 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
• Grabe, Immo; Jaghoori, Mohammad Mahdi; Aichernig, Bernhard; Baier, Cristel; Blechmann, Tobias & Boer, Frank de [Show all 18 contributors for this article] (2010). Credo Methodology: Modeling and Analyzing A Peer-to-Peer System in Credo. Electronical Notes in Theoretical Computer Science. 266, p. 33–48. Full text in Research Archive
• Schlatte, Rudolf; Aichernig, Bernhard K.; Griesmayer, Andreas & Kyas, Marcel (2010). Resource Modeling for Timed Creol Models. Electronical Notes in Theoretical Computer Science. 266, p. 63–75. doi: 10.1016/j.entcs.2010.08.049. Full text in Research Archive Show summary

  This paper describes the semantics of a timed, resource-constrained extension of the Creol modeling language. Creol is an object-oriented modeling language with a design that is suited for modeling distributed systems. However, the computation model of Creol assumes infinite memory and infinite parallelism within an object. This paper describes a way to extend Creol with a notion of resource constraints and a way to quantitatively assess the effects of introducing resource constraints on a given model. We discuss possible semantics of message delivery under resource constraints, their implementation and their impact on the model. The method is illustrated with a case study modeling a biomedical sensor network.

View all works in NVA

• Schlatte, Rudolf (2020). Reversible Computation: Extending Horizons of Computing - Selected Results of the COST Action IC1405. Springer. ISBN 9783030473600. 237 p. Full text in Research Archive

View all works in NVA

• 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
• Mezzina, Claudio Antares; Schlatte, Rudolf; Glück, Robert; Haulund, Tue; Hoey, James & Cservenka, Martin Holm [Show all 11 contributors for this article] (2020). Software and Reversible Systems: A Survey of Recent Activities, Reversible Computation: Extending Horizons of Computing - Selected Results of the COST Action IC1405. Springer. ISSN 9783030473600. p. 41–59. doi: 10.1007/978-3-030-47361-7_2. Full text in Research Archive
• Soylu, Ahmet; Giese, Martin; Jimenez-Ruiz, Ernesto; Kharlamov, Evgeny; Schlatte, Rudolf & Neuenstadt, Christian [Show all 11 contributors for this article] (2016). Ontology-based Visual Querying with OptiqueVQS: Statoil and Siemens Cases. CEUR Workshop Proceedings. 1818. Full text in Research Archive
• Grabe, Immo; Jaghoori, Mohammad Mahdi; Aichernig, Bernhard; Baier, Christel; Blechmann, Tobias & Boer, de Frank [Show all 24 contributors for this article] (2009). Credo methodology - Modeling and analyzing a peer-to-peer system in Credo. Full text in Research Archive
• Kamburjan, Eduard; Klungre, Vidar; Schlatte, Rudolf; Johnsen, Einar Broch & Giese, Martin (2021). Programming and Debugging with Semantically Lifted States (Full Paper). Universitetet i Oslo. Institutt for informatikk. ISSN 9788273684646. Full text in Research Archive Show summary

  We propose a novel integration of programming languages with semantic technologies. We create a semantic reflection mechanism by a direct mapping from program states to RDF knowledge graphs. This mechanism enables several promising novel applications including the use of semantic technology, including reasoning, for debugging and validating the sanity of program states, and integration with external knowledge graphs. Additionally, by making the knowledge graph accessible from the program, method implementations can refer to state semantics rather than objects, establishing a deep integration between programs and semantics. This allows the programmer to use domain knowledge formalized as, e.g., an ontology directly in the program’s control flow. We formalize this integration by defining a core object based programming language that incorporates these features. A prototypical interpreter is available for download.

• Leister, Wolfgang; Bjørk, Joakim; Schlatte, Rudolf & Griesmayer, Andreas (2010). Validation of Creol Models for Routing Algorithms in Wireless Sensor Networks. Norsk Regnesentral. ISSN 9788253905341. Full text in Research Archive Show summary

  We validate a Creol model of AODV by evaluating functional properties using simulation and component testing. We define a structure for evaluating and validating models of wireless sensor networks, which we intend to use as a reference for future evaluations of algorithms.We use the categories of techniques, perspectives, arrangements and properties to structure the evaluation work. We show, by way of the AODV algorithm, how network simulations and component testing can be employed to evaluate a large list of properties. We also show which properties are most suited to be evaluated by which technique, perspective, and arrangement.

View all works in NVA