Rudolf Schlatte

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

  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.

• Schlatte, Rudolf; Johnsen, Einar Broch; Kamburjan, Eduard & Tapia Tarifa, Silvia Lizeth (2022). The ABS simulator toolchain. Science of Computer Programming. ISSN 0167-6423. 223. doi: 10.1016/j.scico.2022.102861.
• Kamburjan, Eduard; Din, Crystal Chang; Schlatte, Rudolf; Tapia Tarifa, Silvia Lizeth & Johnsen, Einar Broch (2022). Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 13701, s. 188–204. doi: 10.1007/978-3-031-19849-6%5C_12.
• Kamburjan, Eduard; Klungre, Vidar Norstein; Schlatte, Rudolf; Tapia Tarifa, Silvia Lizeth; Cameron, David & Johnsen, Einar Broch (2022). Digital Twin Reconfiguration Using Asset Models. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 13704, s. 71–88. doi: 10.1007/978-3-031-19762-8%5C_6.
• Horn, Geir; Schlatte, Rudolf & Johnsen, Einar Broch (2022). Digital Twins for Autonomic Cloud Application Management. I Barolli, Leonard; Hussain, Farookh & Enokido, Tomoya (Red.), Advanced Information Networking and Applications: Proceedings of the 36th International Conference on Advanced Information Networking and Applications (AINA-2022), Volume 3. Springer. ISSN 978-3-030-99618-5. s. 141–152. doi: 10.1007/978-3-030-99619-2_14.
• Kamburjan, Eduard; Schlatte, Rudolf; Johnsen, Einar Broch & Tapia Tarifa, Silvia Lizeth (2021). Designing Distributed Control with Hybrid Active Objects. I Margaria, Tiziana & Steffen, Bernhard (Red.), 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 978-3-030-83722-8. s. 88–108. doi: 10.1007/978-3-030-83723-5_7.
• Schlatte, Rudolf; Johnsen, Einar Broch; Kamburjan, Eduard & Tapia Tarifa, Silvia Lizeth (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.
• de Boer, Frank; Johnsen, Einar Broch; Schlatte, Rudolf; Tapia Tarifa, Silvia Lizeth & Tveito, Lars (2020). Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages. OpenAccess Series in Informatics. ISSN 2190-6807. 86, s. 10:1–10:18. doi: 10.4230/OASIcs.Gabbrielli.10. Fulltekst i vitenarkiv
• Tveito, Lars; Johnsen, Einar Broch & Schlatte, Rudolf (2020). Global Reproducibility Through Local Control for Distributed Active Objects. I Wehrheim, Heike & Cabot, Jordi (Red.), 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 978-3-030-45233-9. s. 140–160. doi: 10.1007/978-3-030-45234-6_7. Fulltekst i vitenarkiv
• Chang Din, Crystal; 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, s. 73–88. doi: 10.1007/978-3-319-92970-5_5. Fulltekst i vitenarkiv
• Schlatte, Rudolf; Johnsen, Einar Broch; Mauro, Jacopo; Tapia Tarifa, Silvia Lizeth & Yu, Ingrid Chieh (2018). Release the Beasts: When Formal Methods Meet Real World Data. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 10865, s. 107–121. doi: 10.1007/978-3-319-90089-6_8.
• 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, s. 379–383. doi: 10.1007/978-3-662-54494-5_22.
• Soylu, Ahmet; Kharlamov, Evgeny; Zheleznyakov, Dmitriy; Jimenez-Ruiz, Ernesto; Giese, Martin & Skjæveland, Martin G [Vis alle 11 forfattere av denne artikkelen] (2017). OptiqueVQS: a Visual Query System over Ontologies for Industry . Semantic Web Journal. ISSN 1570-0844. s. 1–28. doi: 10.3233/sw-180293. Fulltekst i vitenarkiv
• Soylu, Ahmet; Giese, Martin; Schlatte, Rudolf; Jimenez-Ruiz, Ernesto; Kharlamov, Evgeny & Özçep, Özgür [Vis alle 8 forfattere av denne artikkelen] (2017). Querying industrial stream-temporal data: An ontology-based visual approach. Journal of Ambient Intelligence and Smart Environments. ISSN 1876-1364. 9(1), s. 77–95. doi: 10.3233/AIS-160415. Fulltekst i vitenarkiv
• Soylu, Ahmet; Giese, Martin; Jimenez-Ruiz, Ernesto; Kharlamov, Evgeny; Schlatte, Rudolf & Neuenstadt, Christian [Vis alle 11 forfattere av denne artikkelen] (2016). Ontology-based visual querying with OptiqueVQS: Statoil and Siemens cases. CEUR Workshop Proceedings. ISSN 1613-0073. 1818, s. 34–39.
• 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, s. 161–166. doi: 10.1007/978-3-319-47602-5_32.
• 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. ISSN 1613-0073. 1588, s. 11–20.
• Johnsen, Einar Broch; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (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), s. 67–91. doi: 10.1016/j.jlamp.2014.07.001.
• Albert, Elvira; de Boer, Frank; Hähnle, Reiner; Johnsen, Einar Broch; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth [Vis alle 7 forfattere av denne artikkelen] (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), s. 323–339. doi: 10.1007/s11761-013-0148-0.
• Johnsen, Einar Broch; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (2014). Deployment variability in delta-oriented models. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 8802, s. 304–319. doi: 10.1007/978-3-662-45234-9_22.
• 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), s. 5–21. doi: 10.1007/978-3-662-45231-8_2.
• Lanese, Ivan; Lienhardt, Michael; Bravetti, Mario; Johnsen, Einar Broch; Schlatte, Rudolf & Stolz, Volker [Vis alle 7 forfattere av denne artikkelen] (2014). Fault Model Design Space for Cooperative Concurrency. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 8803(2), s. 22–36. doi: 10.1007/978-3-662-45231-8_3.
• Johnsen, Einar Broch; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (2013). Modeling Application-Level Management of Virtualized Resources in ABS. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7542, s. 89–108. doi: 10.1007/978-3-642-35887-6_5.
• Kharlamov, Evgeny; Jimenez-ruiz, Ernesto; Zheleznyakov, Dmitriy; Bilidas, Dimitris; Giese, Martin & Haase, Peter [Vis alle 16 forfattere av denne artikkelen] (2013). Optique: Towards OBDA Systems for Industry. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7955, s. 125–140. doi: 10.1007/978-3-642-41242-4_11.
• Giese, Martin; Calvanese, Diego; Haase, Peter; Horrocks, Ian; Ioannidis, Yannis & Kllapi, Herald [Vis alle 16 forfattere av denne artikkelen] (2013). Scalable End-user Access to Big Data. I Akerkar, Rajendra (Red.), Big Data Computing. Taylor & Francis. ISSN 978-1-46-657837-1. doi: 10.1201/b16014-9.
• Nobakht, Behrooz; de Boer, Frank S.; Jaghoori, Mohammad Mahdi & Schlatte, Rudolf (2012). Programming and deployment of active objects with application-level scheduling. I Ossowski, Sascha & Lecca, Paola (Red.), Proceedings of the 27th Annual ACM Symposium on Applied Computing. Association for Computing Machinery (ACM). ISSN 978-1-4503-0857-1. s. 1883–1888. doi: 10.1145/2245276.2232086.
• 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), s. 567–588. doi: 10.1007/s10009-012-0250-1. Vis sammendrag

  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.

• Johnsen, Einar Broch; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (2012). A Formal Model of Object Mobility in Resource-Restricted Deployment Scenarios. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7253, s. 187–204. doi: 10.1007/978-3-642-35743-5_12.
• Johnsen, Einar Broch; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (2012). A Formal Model of User-Defined Resources in Resource-Restricted Deployment Scenarios. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7421, s. 196–213. doi: 10.1007/978-3-642-31762-0_13.
• de Boer, Frank; 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, s. 91–106. doi: 10.1007/978-3-642-33427-6_7.
• Johnsen, Einar Broch; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (2012). Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7635, s. 71–86. doi: 10.1007/978-3-642-34281-3_8.
• Bjørk, Joakim; de Boer, Frank; Johnsen, Einar Broch; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (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.
• 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. ISSN 1942-2601. 5(1&2), s. 55–68. Vis sammendrag

  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.

• 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, s. 204–224. doi: 10.1007/978-3-642-25271-6_11. Vis sammendrag

  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.

• Schlatte, Rudolf; Johnsen, Einar Broch; Kazemeyni, Fatemeh Sadat & Tapia Tarifa, Silvia Lizeth (2011). Models of Rate Restricted Communication for Concurrent Objects. Electronical Notes in Theoretical Computer Science. ISSN 1571-0661. 274, s. 67–81. doi: 10.1016/j.entcs.2011.07.007.
• Johnsen, Einar Broch; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (2011). Integrating Aspects of Software Deployment in High-Level Executable Models, Norsk Informatikkonferanse NIK 2011. Tapir Akademisk Forlag. ISSN 978-82-519-2843-4.
• Clarke, Dave; Diakov, Nikolay; Hähnle, Reiner; Johnsen, Einar Broch; Schaefer, Ina & Schäfer, Jan [Vis alle 8 forfattere av denne artikkelen] (2011). Modeling Spatial and Temporal Variability with the HATS Abstract Behavioral Modeling Language. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6659, s. 417–457. doi: 10.1007/978-3-642-21455-4_13.
• Albert, Elvira; Genaim, Samir; Gómez-Zamalloa, Miguel; Johnsen, Einar Broch; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (2011). Simulating Concurrent Behaviors with Worst-Case Cost Bounds. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6664, s. 353–368. doi: 10.1007/978-3-642-21437-0_27.
• 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.
• 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 978-1-61208-005-5.
• Johnsen, Einar Broch; Owe, Olaf; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (2011). Validating Timed Models of Deployment Components with Parametric Concurrency. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6528, s. 46–60. doi: 10.1007/978-3-642-18070-5_4.
• Grabe, Immo; Jaghoori, Mohammad Mahdi; Klein, Joachim; Klüppelholz, Sascha; Stam, Andries & Baier, Christel [Vis alle 18 forfattere av denne artikkelen] (2010). The Credo Methodology (Extended Version). Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6286, s. 41–69.
• Johnsen, Einar Broch; Owe, Olaf; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (2010). Deployment Components with Parametric Concurrency. I Walden, Marina & Petre, Luigia (Red.), Proceedings of the 22nd Nordic Workshop on Programming Theory, NWPT'10. TUCS. ISSN 978-952-12-2478-2. s. 23–25.
• Schlatte, Rudolf; Aichernig, Bernhard K.; Griesmayer, Andreas & Kyas, Marcel (2010). Resource Modeling for Timed Creol Models. Electronical Notes in Theoretical Computer Science. ISSN 1571-0661. 266, s. 63–75. doi: 10.1016/j.entcs.2010.08.049. Vis sammendrag

  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.

• Grabe, Immo; Jaghoori, Mohammad Mahdi; Aichernig, Bernhard; Baier, Cristel; Blechmann, Tobias & de Boer, Frank [Vis alle 18 forfattere av denne artikkelen] (2010). Credo Methodology: Modeling and Analyzing A Peer-to-Peer System in Credo. Electronical Notes in Theoretical Computer Science. ISSN 1571-0661. 266, s. 33–48.
• Johnsen, Einar Broch; Owe, Olaf; Schlatte, Rudolf & Tapia Tarifa, Silvia Lizeth (2010). Dynamic Resource Reallocation between Deployment Components. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 6447, s. 646–661.
• Bjørk, Joakim; Johnsen, Einar Broch; Owe, Olaf & Schlatte, Rudolf (2010). Lightweight Time Modeling in Timed Creol. Electronic Proceedings in Theoretical Computer Science (EPTCS). ISSN 2075-2180. 36, s. 67–81.

Se alle arbeider i Cristin

• Schlatte, Rudolf (2020). Reversible Computation: Extending Horizons of Computing - Selected Results of the COST Action IC1405. Springer. ISBN 978-3-030-47360-0. 237 s.

Se alle arbeider i Cristin

• Mezzina, Claudio Antares; Schlatte, Rudolf; Glück, Robert; Haulund, Tue; Hoey, James & Cservenka, Martin Holm [Vis alle 11 forfattere av denne artikkelen] (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 978-3-030-47360-0. s. 41–59. doi: https%3A/doi.org/10.1007/978-3-030-47361-7_2.
• Soylu, Ahmet; Giese, Martin; Jimenez-Ruiz, Ernesto; Kharlamov, Evgeny; Schlatte, Rudolf & Neuenstadt, Christian [Vis alle 11 forfattere av denne artikkelen] (2016). Ontology-based Visual Querying with OptiqueVQS: Statoil and Siemens Cases. CEUR Workshop Proceedings. ISSN 1613-0073. 1818.
• Grabe, Immo; Jaghoori, Mohammad Mahdi; Aichernig, Bernhard; Baier, Christel; Blechmann, Tobias & Boer, de Frank [Vis alle 24 forfattere av denne artikkelen] (2009). Credo methodology - Modeling and analyzing a peer-to-peer system in Credo.
• Kamburjan, Eduard; Klungre, Vidar; Schlatte, Rudolf; Johnsen, Einar Broch & Giese, Martin (2021). Programming and Debugging with Semantically Lifted States (Full Paper). Springer. ISSN 978-82-7368-464-6. Fulltekst i vitenarkiv
• Leister, Wolfgang; Bjørk, Joakim; Schlatte, Rudolf & Griesmayer, Andreas (2010). Validation of Creol Models for Routing Algorithms in Wireless Sensor Networks. Norsk Regnesentral. ISSN 978-82-539-0534-1. Vis sammendrag

  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.

Se alle arbeider i Cristin