Olaf Owe

• Foroughi, Mehdi; Bagherpour, Matin; Eliassen, Frank & Owe, Olaf (2026). PSDO: Privacy-Preserving Distributed Optimization for Autonomous Prosumer Energy Management. IEEE Transactions on Dependable and Secure Computing. ISSN 1545-5971. 23(3), p. 6874–6889. doi: 10.1109/tdsc.2026.3669022. Full text in Research Archive Show summary

  In the evolving energy landscape where prosumers play an increasingly important role, establishing a secure data exchange architecture is essential for building a resilient and efficient energy infrastructure. Current privacy-preserving systems suffer from inadequate adversarial models, dependence on centralized components, and inability to adapt to evolving threats. This paper introduces the Privacy-Sensitive Distributed Optimization (PSDO) framework, a decentralized management scheme designed to prioritize privacy safeguards in prosumer-driven systems. To achieve this goal, the PSDO framework combines decentralized optimization techniques with differential privacy. This integration serves a dual purpose: preserving prosumers’ control over their energy management and ensuring privacy of their sensitive information. By leveraging decentralized optimization, the PSDO framework enables prosumers to maximize the benefits derived from decentralized systems, promoting improved autonomy in energy management. Simultaneously, prosumers’ sensitive data is protected through the implementation of differential privacy measures. Through implementation on the IEEE 33-bus radial distribution system, the PSDO algorithm demonstrated its capability to converge to the optimal solution while rigorously upholding differential privacy. PSDO advances beyond the chosen baseline (DP-ADMM) by delivering superior privacy protection while incurring minimal utility loss. Moreover, the framework successfully accommodates diverse privacy preferences while maintaining system-wide efficiency, establishing its effectiveness for heterogeneous prosumers.

• Owe, Olaf (2025). On the Development of the Active Object Paradigm: A Personal Account. In Meseguer, Jose; Varela, Carlos A. & Venkatasubramanian, Nalini (Ed.), Concurrent Programming, Open Systems and Formal Methods. Springer Nature Switzerland. ISSN 9783032052919. p. 114–143. doi: 10.1007/978-3-032-05291-9_5. Full text in Research Archive Show summary

  This paper gives a personal account of research activity performed over decades by the author and his collaborators towards developing expressive and efficient object-oriented language paradigms for distributed systems. The goal is to enable expressive and efficient programs with a mathematically simple semantics, so that programming and verification are as simple as possible. Starting from traditional object-oriented principles, the paper suggests ways to deal with major challenges related to concurrency, communication, inheritance, flexibility of code reuse, and openness. The resulting language can be classified as an active object language, which can be seen as a modernization of object orientation for concurrent systems. The language integrates several aspects of the Actor Model in an object-oriented, imperative setting. The focus of the paper is simplicity of modeling, specification, and reasoning. Behavioral subtyping is replaced by the more liberal concept of interface behavioral subtyping, and a renewed notion of subclass inheritance allows unrestricted reuse of code and specifications, supported by reasoning control. These benefits are shown useful for subclassing as well as for program evolution. A notion of hierarchy independence limits reverification in the case of multiple inheritance, so that only changed classes and subclasses inheriting from them need to be reverified.

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

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

• Arshad, Hamed; Horne, Ross; Johansen, Christian; Owe, Olaf & Willemse, Tim A.C. (2024). XACML2mCRL2: Automatic transformation of XACML policies into mCRL2 specifications[Formula presented]. Science of Computer Programming. ISSN 0167-6423. 232. doi: 10.1016/j.scico.2023.103046. Full text in Research Archive
• 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.

• Owe, Olaf & Fazeldehkordi, Elahe (2022). A lightweight approach to smart contracts supporting safety, security, and privacy. Journal of Logical and Algebraic Methods in Programming. ISSN 2352-2208. 127. doi: 10.1016/j.jlamp.2022.100772. Full text in Research Archive
• Arshad, Hamed; Horne, Ross; Johansen, Christian; Owe, Olaf & Willemse, Tim A. C. (2022). Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies Using mCRL2. In Mousavi, Mohammad Reza & Philippou, Anna (Ed.), Formal Techniques for Distributed Objects, Components, and Systems. 42nd IFIP WG 6.1 International Conference, FORTE 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, June 13–17, 2022, Proceedings. Springer. ISSN 9783031086793. p. 11–30. doi: 10.1007/978-3-031-08679-3_2. Full text in Research Archive
• Arshad, Hamed; Johansen, Christian & Owe, Olaf (2022). Semantic Attribute-Based Access Control: A review on current status and future perspectives. Journal of systems architecture. ISSN 1383-7621. 129. doi: 10.1016/j.sysarc.2022.102625. Full text in Research Archive
• Arshad, Hamed; Johansen, Christian; Owe, Olaf; Picazo-Sanchez, Pablo & Schneider, Gerardo (2022). Semantic Attribute-Based Encryption: A framework for combining ABE schemes with semantic technologies. Information Sciences. ISSN 0020-0255. doi: 10.1016/j.ins.2022.10.132. Full text in Research Archive
• 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.

• Tokas, Shukun; Owe, Olaf & Ramezanifarkhani, Toktam (2021). Static checking of GDPR-related privacy compliance for object-oriented distributed systems. Journal of Logical and Algebraic Methods in Programming. ISSN 2352-2208. 125. doi: 10.1016/j.jlamp.2021.100733. Full text in Research Archive Show summary

  The adoption of information technology in foremost sectors of human activity such as banking, healthcare, education, governance etc., increases the amount of data collected and processed to enable these services. With the convenience the technology offers, it also brings increased challenges pertaining to the privacy. In response to these emerging privacy concerns, the European Union has approved the General Data Protection Regulation (GDPR) to strengthen data protection across the European Union. This regulation requires individuals and organizations that process personal data of EU citizens or provide services in EU, to comply with the privacy requirements in the GDPR. However, the privacy policies stating how personal information will be handled to meet regulations as well as organizational objectives, are given in natural language statements. To demonstrate a program's compliance with privacy policies, a link should be established between policy statements and the program code, with the support of a formalized analysis. Based on this vision, we formalize a notion of privacy policies and a notion of compliance for the setting of object-oriented distributed systems. For this we provide explicit constructs to specify constituents of privacy policies (i.e., principal, purpose, access right) on personal data. We present a policy specification language and a formalization of privacy compliance, as well as a high-level modeling language for distributed systems extended with support for policies. We define a type and effect system for static checking of compliance of privacy policies and show soundness of this analysis based on an operational semantics. Finally, we prove a progress property.

• Tokas, Shukun; Owe, Olaf & Ramezanifarkhani, Toktam (2020). Language-based mechanisms for privacy-by-design. In Friedewald, Michael (Eds.), Privacy and Identity Management. Data for Better Living: AI and Privacy. Springer Nature. ISSN 9783030425036. p. 142–158. doi: 10.1007/978-3-030-42504-3_10. Full text in Research Archive Show summary

  The privacy by design principle has been applied in system engineering. In this paper, we follow this principle, by integrating necessary safeguards into the program system design. These safeguards are then used in the processing of personal information. In particular, we use a formal language-based approach with static analysis to enforce privacy requirements. To make a general solution, we consider a high-level modeling language for distributed service-oriented systems, building on the paradigm of active objects. The language is then extended to support specification of policies on program constructs and policy enforcement. For this we develop i) language constructs to formally specify privacy restrictions, thereby obtaining a policy definition language, ii) a formal notion of policy compliance, and iii) a type and effect system for enforcing and analyzing a program’s compliance with the stated polices.

• Tokas, Shukun & Owe, Olaf (2020). A Formal Framework for Consent Management. In Sokolova, Ana (Eds.), Formal Techniques for Distributed Objects, Components, and Systems (40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020, Proceedings). Springer Nature. ISSN 9783030500863. p. 169–186. doi: 10.1007/978-3-030-50086-3_10. Full text in Research Archive Show summary

  The aim of this work is to design a formal framework for consent management in line with EU’s General Data Protection Regulation (GDPR). To make a general solution, we consider a high-level modeling language for distributed service-oriented systems, building on the paradigm of active objects. Our framework provides a general solution for data subjects to observe and change their privacy settings and to be informed about all personal data stored about them. The solution consists of a set of predefined types for privacy related concepts, a formalization of policy compliance, a set of interfaces that forms the basis of interaction with external users for consent management, a set of classes that is used in interaction with the runtime system, and a runtime system enforcing the consented policies.

• Owe, Olaf; Fazeldehkordi, Elahe & Lin, Jia-Chun (2020). A Framework for Flexible Program Evolution and Verification of Distributed Systems. Communications in Computer and Information Science (CCIS). ISSN 1865-0929. 1161 CCIS, p. 320–349. doi: 10.1007/978-3-030-37873-8_14. Full text in Research Archive Show summary

  Program evolution may reveal bad design decisions, misunderstandings, erroneous code, or erroneous specifications, because problems made early in the design of a system may not be discovered until much later in the life-time of the system. Non-trivial changes of old code may be necessary. Flexibility in making such changes is essential, especially in a distributed setting where the system components are updated independently. In this setting re-verification is challenging. We consider flexibility with respect to what changes can be made as well as what can be efficiently reverified. In this paper we propose a flexible framework for modeling and evolution of distributed systems. It supports unrestricted modifications in such systems, both in code and specifications, and with support of verification and re-verification. We consider on the setting of concurrent and object-oriented distributed programs, and introduce a core high-level modeling language supporting active objects. We allow multiple inheritance because it gives added flexibility during evolution, allowing a wider class of software changes. To avoid undesired effects of multiple inheritance, we apply a healthy binding strategy. We prove that the framework supports Modification Independence and Hierarchy Independence, which requires healthy binding. We demonstrate that our framework can deal with verification of software changes that are not possible in comparable frameworks.

• Fazeldehkordi, Elahe; Owe, Olaf & Ramezanifarkhani, Toktam (2020). A Language-Based Approach to Prevent DDoS Attacks in Distributed Financial Agent Systems. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 11981 LNCS, p. 258–277. doi: 10.1007/978-3-030-42051-2_18. Full text in Research Archive
• Tokas, Shukun & Owe, Olaf (2019). A Formal Framework for Consent Management. In Uustalu, Tarmo (Eds.), Proceedings of the 31st Nordic Workshop on Programming Theory. Tallinn University of Technology. ISSN 9789949835201. p. 73–76. Full text in Research Archive
• Karami, Farzane; Owe, Olaf & Ramezanifarkhani, Toktam (2019). Summary of: An Evaluation of Interaction Paradigms for Active Objects. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 11918, p. 529–533. doi: 10.1007/978-3-030-34968-4_31. Full text in Research Archive Show summary

  Sammendrag

• Johansen, Christian & Owe, Olaf (2019). Dynamic Structural Operational Semantics. Journal of Logical and Algebraic Methods in Programming. ISSN 2352-2208. 107, p. 79–107. doi: 10.1016/j.jlamp.2019.05.006. Full text in Research Archive Show summary

  We introduce Dynamic Structural Operational Semantics (DSOS or Dynamic SOS) as a framework for describing semantics of programming languages that include dynamic software upgrades, i.e., for upgrading software code during run-time. DSOS is built on top of the Modular SOS of P. Mosses, with an underlying category theory formalization. The idea of Dynamic SOS is to bring out the essential differences between dynamic upgrade constructs and program execution constructs. The important feature of Modular SOS (MSOS) that we exploit in DSOS is the sharp separation of the program execution code from the additional (data) structures needed at run-time. In DSOS we aim to achieve the same modularity and decoupling for dynamic software upgrades. This is partly motivated by the long term goal of having machine-checkable proofs for general results like type safety. We exemplify Dynamic SOS on two languages supporting dynamic software upgrades, namely the C-like Proteus, which supports updating of variables, functions, records, or types at specific program points, and Creol, which supports dynamic class upgrades in the setting of concurrent objects. Existing type analyses for software upgrades can be done on top of DSOS too, as we illustrate for Proteus. As a side contribution we define a general encapsulating construction on Modular SOS useful in situations where a form of encapsulation of the execution is needed. We use encapsulation to give modular semantics to the concurrent object-oriented programming language Creol with active objects and asynchronous method invocations.

• Johansen, Christian & Owe, Olaf (2019). Summary of: Dynamic Structural Operational Semantics. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 11918, p. 525–528. doi: 10.1007/978-3-030-34968-4_30. Full text in Research Archive
• Fazeldehkordi, Elahe; Owe, Olaf & Noll, Josef (2019). Security and privacy in iot systems: A case study of healthcare products. International Symposium on Medical Information and Communication Technology. ISSN 2326-828X. 2019-May. doi: 10.1109/ISMICT.2019.8743971. Full text in Research Archive
• Lee, Ming-Chang; Lin, Jia-Chun & Owe, Olaf (2019). PDS: Deduce elder privacy from smart homes. Internet of Things: Engineering Cyber Physical Human Systems. 7. doi: 10.1016/j.iot.2019.100072. Full text in Research Archive Show summary

  With the development of IoT technologies in the past few years, a wide range of smart devices are deployed in a variety of environments aiming to improve the quality of human life in a cost efficient way. Due to the increasingly serious aging problem around the world, smart homes for elder healthcare have become an important IoT-based application, which not only enables elders’ health to be properly monitored and taken care of, but also allows them to live more comfortably and independently in their houses. However, elders’ privacy might be disclosed from smart homes due to non-fully protected network communication. To show that elders’ privacy could be substantially exposed, in this paper we develop a Privacy Deduction Scheme (PDS for short) by eavesdropping sensor traffic from a smart home to identify elders’ movement activities and speculating sensor locations in the smart home based on a series of deductions from the viewpoint of an attacker. The experimental results based on sensor datasets from real smart homes demonstrate the effectiveness of PDS in deducing and disclosing elders’ privacy, which might be maliciously exploited by attackers to endanger elders and their properties.

• Owe, Olaf; Lin, Jia-Chun & Fazeldehkordi, Elahe (2019). A Flexible Framework for Program Evolution and Verification. In Hammoudi, Slimane; Pires, Luís Ferreira & Selic, Bran (Ed.), Modelsward 2019. SciTePress. ISSN 9789897583582. p. 179–191. doi: 10.5220/0007690301770189. Full text in Research Archive
• Tokas, Shukun; Owe, Olaf & Ramezanifarkhani, Toktam (2018). Language-Based Support for GDPR-Related Privacy Requirements. In Fava, Daniel Schnetzer; Johnsen, Einar Broch & Owe, Olaf (Ed.), Proceedings of the 30th Nordic Workshop on Programming Theory. Universitetet i Oslo. ISSN 9788273684509. p. 70–72. Full text in Research Archive
• Din, Crystal Chang; Johnsen, Einar Broch; Owe, Olaf & Yu, Ingrid Chieh (2018). A modular reasoning system using uninterpreted predicates for code reuse. Journal of Logical and Algebraic Methods in Programming. ISSN 2352-2208. 95, p. 82–102. doi: 10.1016/j.jlamp.2017.11.004. Full text in Research Archive Show summary

  This paper proposes a modular proof system based on uninterpreted predicates. The proposed proof system allows modular reasoning about programs with an open-world assumption, which goes beyond behavioral subtyping. The proof system enables modular reasoning about languages with very flexible code reuse mechanisms, such as traits and deltas in the context of object-oriented programming. Whereas related work on incremental proof systems prove soundness in terms of internal consistency, this paper establishes both soundness and relative completeness of the proposed proof system by relating it to a standard proof system for a simple object-oriented language. The applicability of the approach is demonstrated on different code reuse mechanisms: unrestricted class inheritance, delta-oriented programming, and trait-based programming.

• Lee, Ming-Chang; Lin, Jia-Chun & Owe, Olaf (2018). EasyChoose: A Continuous Feature Extraction and Review Highlighting Scheme on Hadoop YARN. Advanced Information Networking and Applications. ISSN 1550-445X. 2018-May, p. 996–1002. doi: 10.1109/AINA.2018.00145. Full text in Research Archive
• Karami, Farzane; Owe, Olaf & Ramezanifarkhani, Toktam (2018). An Evaluation of Interaction Paradigms for Active Objects. Journal of Logical and Algebraic Methods in Programming. ISSN 2352-2208. 103, p. 154–183. doi: 10.1016/j.jlamp.2018.11.008. Full text in Research Archive
• Ramezanifarkhani, Toktam; Owe, Olaf & Tokas, Shukun (2018). A secrecy-preserving language for distributed and object-oriented systems. Journal of Logical and Algebraic Methods in Programming. ISSN 2352-2208. 99, p. 1–25. doi: 10.1016/j.jlamp.2018.04.001. Full text in Research Archive Show summary

  In modern systems it is often necessary to distinguish between confidential (low-level) and non-confidential (high-level) information. Confidential information should be protected and not communicated or shared with low-level users. The non-interference policy is an information flow policy stipulating that low-level viewers should not be able to observe a difference between any two executions with the same low-level inputs. Only high-level viewers may observe confidential output. This is a non-trivial challenge when considering modern distributed systems involving concurrency and communication. The present paper addresses this challenge, by choosing language mechanisms that are both useful for programming of distributed systems and allow modular system analysis. We consider a general concurrency model for distributed systems, based on concurrent objects communicating by asynchronous methods. This model is suitable for modeling of modern service-oriented systems, and gives rise to efficient interaction avoiding active waiting and low-level synchronization primitives such as explicit signaling and lock operations. This concurrency model has a simple semantics and allows us to focus on information flow at a high level of abstraction, and allows realistic analysis by avoiding unnecessary restrictions on information flow between confidential and non-confidential data. Due to the non-deterministic nature of concurrent and distributed systems, we define a notion of interaction non-interference policy tailored to this setting. We provide two kinds of static analysis: a secrecy-type system and a trace analysis system, to capture inter-object and network level communication, respectively. We prove that interaction non-interference is satisfied by the combination of these analysis techniques. Thus any deviation from the policy caused by implicit information leakage visible through observation of network communication patterns, can be detected. The contribution of the paper lies in the definition of the notion of interaction non-interference, and in the formalization of a secrecy type system and a static trace analysis that together ensure interaction non-interference. We also provide several versions of a main example (a news subscription service) to demonstrate network leakage.

• Lee, Ming-Chang; Lin, Jia-Chun & Owe, Olaf (2018). Privacy Mining from IoT-based Smart Homes (Online version). Lecture Notes on Data Engineering and Communications Technologies. ISSN 2367-4512. p. 304–315. doi: 10.1007/978-3-030-02613-4_27. Full text in Research Archive
• Ramezanifarkhani, Toktam; Fazeldehkordi, Elahe & Owe, Olaf (2017). A Language-Based Approach to Prevent DDoS Attacks in Distributed Object Systems. In Walden, Marina (Eds.), Proceedings of the 29th Nordic Workshop on Programming Theory. Turku Centre for Computer Science. ISSN 9789521236082. p. 19–21. Full text in Research Archive
• Ramezanifarkhani, Toktam; Karami, Farzane & Owe, Olaf (2017). A High-Level Language for Active Objects with Future-Free Support of Futures. In Walden, Marina (Eds.), Proceedings of the 29th Nordic Workshop on Programming Theory. Turku Centre for Computer Science. ISSN 9789521236082. p. 25–27. Full text in Research Archive
• Tokas, Shukun; Owe, Olaf & Johansen, Christian (2017). Code Diversification Mechanisms for Securing the Internet of Things. In Walden, Marina (Eds.), Proceedings of the 29th Nordic Workshop on Programming Theory. Turku Centre for Computer Science. ISSN 9789521236082. p. 10–12. Full text in Research Archive
• Owe, Olaf & Ramezanifarkhani, Toktam (2017). Confidentiality of Interactions in Concurrent Object-Oriented Systems. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 10436, p. 19–34. doi: 10.1007/978-3-319-67816-0_2. Full text in Research Archive
• Owe, Olaf; Ramezanifarkhani, Toktam & Fazeldehkordi, Elahe (2017). Hoare-style Reasoning from Multiple Contracts. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 10510, p. 263–278. doi: 10.1007/978-3-319-66845-1_17. Full text in Research Archive
• Owe, Olaf & McDowell, Charlie (2017). On Detecting Over-Eager Concurrency in Asynchronously Communicating Concurrent Object Systems. Journal of Logical and Algebraic Methods in Programming. ISSN 2352-2208. 90, p. 158–175. doi: 10.1016/j.jlamp.2017.02.005. Full text in Research Archive
• Owe, Olaf (2016). Verifiable Programming of Object-Oriented and Distributed Systems. In Petre, Luigia & Sekerinski, Emil (Ed.), From Action Systems to Distributed Systems: The Refinement Approach. CRC Press. ISSN 9781498701587. p. 61–79. doi: 10.1201/b20053-8. Full text in Research Archive
• Owe, Olaf (2016). Reasoning about inheritance and unrestricted reuse in object-oriented concurrent systems. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 9681, p. 210–225. doi: 10.1007/978-3-319-33693-0_14. Full text in Research Archive
• Bubel, Richard; Damiani, Ferruccio; Hähnle, Reiner; Johnsen, Einar Broch; Owe, Olaf & Schaefer, Ina [Show all 7 contributors for this article] (2016). Proof Repositories for Compositional Verification of Evolving Software Systems - Managing Change When Proving Software Correct. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 9960, p. 130–156. doi: 10.1007/978-3-319-46508-1_8. Full text in Research Archive
• Johnsen, Einar Broch; Owe, Olaf; Clarke, Dave & Bjørk, Joakim (2016). A formal model of service-oriented dynamic object groups. Science of Computer Programming. ISSN 0167-6423. 115-116, p. 3–22. doi: 10.1016/j.scico.2014.11.014. Full text in Research Archive
• Dovland, Johan; Johnsen, Einar Broch; Owe, Olaf & Yu, Ingrid Chieh (2015). A proof system for adaptable class hierarchies. Journal of Logical and Algebraic Methods in Programming. ISSN 2352-2208. 84(1), p. 37–53. doi: 10.1016/j.jlamp.2014.09.001. Full text in Research Archive
• Din, Crystal Chang & Owe, Olaf (2015). Compositional reasoning about active objects with shared futures. Formal Aspects of Computing. ISSN 0934-5043. 27(3), p. 551–572. doi: 10.1007/s00165-014-0322-y. Full text in Research Archive
• Kazemeyni, Fatemeh Sadat; Owe, Olaf; Johnsen, Einar Broch & Balasingham, Ilangko (2014). Formal modeling and analysis of learning-based routing in mobile wireless sensor networks. Advances in Intelligent Systems and Computing. ISSN 2194-5357. 263, p. 127–150. doi: 10.1007/978-3-319-04717-1_6. Full text in Research Archive
• Din, Crystal Chang; Owe, Olaf & Bubel, Richard (2014). Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. In Filipe, Joaquim & Neves, R. (Ed.), Proc. International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2014. SciTePress. ISSN 9789898565426. p. 480–487. doi: 10.5220/0004877804800487. Full text in Research Archive
• Din, Crystal Chang & Owe, Olaf (2014). A sound and complete reasoning system for asynchronous communication with shared futures. Journal of Logic and Algebraic Programming. ISSN 1567-8326. 83(5-6), p. 360–383. doi: 10.1016/j.jlamp.2014.03.003. Full text in Research Archive
• Owe, Olaf & Yu, Ingrid Chieh (2014). Deadlock detection of active objects with synchronous and asynchronous method calls. NIKT: Norsk IKT-konferanse for forskning og utdanning. ISSN 1892-0713. 3. doi: 10.1016/j.entcs.2004.06.012. Full text in Research Archive
• Kazemeyni, Fatemeh Sadat; Owe, Olaf; Johnsen, Einar Broch & Balasingham, Ilangko (2013). Learning-based routing in mobile wireless sensor networks: Applying formal modeling and analysis. In Zhang, Chengcui & al, . et (Ed.), IEEE 14th International Conference on Information Reuse & Integration, IRI 2013, San Francisco, CA, USA. IEEE (Institute of Electrical and Electronics Engineers). ISSN 9781479910502. p. 504–511. doi: 10.1109/IRI.2013.6642512. Full text in Research Archive
• Din, Crystal Chang; Bubel, Richard & Owe, Olaf (2013). A comparison of runtime assertion checking and theorem proving forconcurrent and distributed systems. In Uustalu, Tarmo & Vain, Jüri (Ed.), 25th Nordic Workshop on Programming TheoryNWPT 2013, Tallinn, Estonia, 20–22 November 2013Abstracts. Institute of Cybernetics at Tallinn University of Technology. ISSN 9789949430703. p. 25–27. Full text in Research Archive
• Johnsen, Einar Broch; Tran, Thi Mai Thuong; Owe, Olaf & Steffen, Martin (2012). Safe Locking for Multi-Threaded Java. In Arbab, Farhad & Sirjani, Marjan (Ed.), Proceedings of FSEN 2011. Springer. ISSN 9783642293191. doi: 10.1007/978-3-642-29320-7_11. Full text in Research Archive
• Johnsen, Einar Broch; Tran, Thi Mai Thuong; Owe, Olaf & Steffen, Martin (2012). Safe locking for multi-threaded Java with exceptions. Journal of Logic and Algebraic Programming. ISSN 1567-8326. 81(3), p. 257–283. doi: 10.1016/j.jlap.2011.11.002. Full text in Research Archive
• Kazemeyni, Fatemeh Sadat; Johnsen, Einar Broch; Owe, Olaf & Balasingham, Ilangko (2012). Formal modeling and validation of a power-efficient grouping protocol for WSNs. Journal of Logic and Algebraic Programming. ISSN 1567-8326. 81(3), p. 284–297. doi: 10.1016/j.jlap.2011.12.001. Full text in Research Archive
• Din, Crystal Chang; Dovland, Johan; Johnsen, Einar Broch & Owe, Olaf (2012). Observable behavior of distributed systems: Component reasoning for concurrent objects. Journal of Logic and Algebraic Programming. ISSN 1567-8326. 81(3), p. 227–256. doi: 10.1016/j.jlap.2012.01.003. Full text in Research Archive
• Damiani, Ferruccio; Dovland, Johan; Johnsen, Einar Broch; Owe, Olaf; Schaefer, Ina & Yu, Ingrid Chieh (2012). A Transformational Proof System for Delta-Oriented Programming, SPLC'12 Proceedings of the 16th International Software Product Line Conference - Volume 2. ACM Publications. ISSN 9781450310956. p. 53–60. doi: 10.1145/2364412.2364422. Full text in Research Archive
• Din, Crystal Chang; Dovland, Johan & Owe, Olaf (2012). Compositional Reasoning about Shared Futures. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7504, p. 94–108. doi: 10.1007/978-3-642-33826-7_7. Full text in Research Archive
• Din, Crystal Chang & Owe, Olaf (2012). Soundness of a Reasoning System for Asynchronous Communication with Futures. In Wolter, Uwe Egbert & Lamo, Yngve (Ed.), 24th Nordic Workshop on Programming Theory. Universitetet i Bergen. doi: 10.1016/j.jlamp.2014.03.003. Full text in Research Archive
• Kazemeyni, Fatemeh Sadat; Johnsen, Einar Broch; Owe, Olaf & Balasingham, Ilangko (2012). MULE-Based Wireless Sensor Networks: Probabilistic Modeling and Quantitative Analysis. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 7321, p. 143–157. doi: 10.1007/978-3-642-30729-4_11. Full text in Research Archive
• Bjørk, Joakim; Clarke, Dave; Johnsen, Einar Broch & Owe, Olaf (2012). A Type-Safe Model of Adaptive Object Groups. Electronic Proceedings in Theoretical Computer Science (EPTCS). 91, p. 1–15. doi: 10.4204/EPTCS.91.1. Full text in Research Archive
• Bentea, Lucian & Owe, Olaf (2012). A Framework for Object-Oriented Modeling and Analysis of Probabilistic Open Distributed Systems. In Beckert, Bernhard; Damiani, Ferruccio & Gurov, Dillan (Ed.), Formal Verification of Object-Oriented Software International Conference, FoVeOOS 2011, Turin, Italy, October 5-7, 2011, Revised Selected Papers. Springer. ISSN 9783642317613. p. 103–120. doi: 10.1007/978-3-642-31762-0_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
• Dovland, Johan; Johnsen, Einar Broch; Owe, Olaf & Steffen, Martin (2011). Incremental reasoning with lazy behavioral subtyping for multiple inheritance. Science of Computer Programming. ISSN 0167-6423. 76(10), p. 915–941. doi: 10.1016/j.scico.2010.09.006. Full text in Research Archive
• Kazemeyni, Fatemeh Sadat; Johnsen, Einar Broch; Owe, Olaf & Balasingham, Ilangko (2011). Group Selection by Nodes in Wireless Sensor Networks Using Coalitional Game Theory. In Perseil, Isabelle; Breitman, Karin & Sterritt, Roy (Ed.), 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011. IEEE (Institute of Electrical and Electronics Engineers). ISSN 9781612848532. p. 253–262. doi: 10.1109/iceccs.2011.32. Full text in Research Archive
• Dovland, Johan; Johnsen, Einar Broch; Owe, Olaf & Yu, Ingrid Chieh (2011). A Proof System for Adaptable Class Hierarchies. In Petterson, Paul & Cristina, Seceleanu (Ed.), Proceedings of the 23rd Nordic Workshop on Programming Theory, NWPT'11. Mälardalen University. ISSN 9789521224782. p. 33–34. doi: 10.1016/j.jlamp.2014.09.001. 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
• Dovland, Johan; Johnsen, Einar Broch; Owe, Olaf & Steffen, Martin (2010). Lazy behavioral subtyping. Journal of Logic and Algebraic Programming. ISSN 1567-8326. 79(7), p. 578–607. doi: 10.1016/j.jlap.2010.07.008. Full text in Research Archive
• Clarke, Dave; Johnsen, Einar Broch & Owe, Olaf (2010). Concurrent Objects a la Carte. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 5930, p. 185–206. Full text in Research Archive

View all works in NVA

• Fava, Daniel Schnetzer; Johnsen, Einar Broch & Owe, Olaf (2018). Proceedings of the 30th Nordic Workshop on Programming Theory. Universitetet i Oslo. ISBN 9788273684509. 84 p. Full text in Research Archive
• Owe, Olaf; Steffen, Martin & Telle, Jan Arne (2011). Fundamentals of Computation Theory - 18th International Symposium, FCT 2011, Oslo, Norway, August 22-25, 2011. Springer. ISBN 9783642229534. 371 p. Full text in Research Archive

View all works in NVA

• Ramezanifarkhani, Toktam; Owe, Olaf & Yu, Ingrid Chieh (2021). Leadership in Academia. Full text in Research Archive
• Fazeldehkordi, Elahe; Owe, Olaf & Noll, Josef (2020). Security and Privacy Functionalities in IoT. In Ghorbani, Ali A (Eds.), 17th International Conference on Privacy, Security and Trust (PST). IEEE (Institute of Electrical and Electronics Engineers). ISSN 9781728132655. doi: 10.1109/PST47121.2019.8949054. Full text in Research Archive
• Karami, Farzane; Owe, Olaf & Schneider, Gerardo (2020). Information-Flow Control by means of Security Wrappers for Active Object Languages with Futures. In Proceedings of The 25th Nordic Conference on Secure IT Systems (NortdSec 2020). To appear in Lecture Notes in Computer Science (17 pages). Full text in Research Archive Show summary

  This paper introduces a run-time mechanism for preventing leakage of secure information in distributed systems. We consider a general concurrency language model where concurrent objects interact by asynchronous method calls and futures. The aim is to prevent leakage of secure information to low-level viewers. The approach is based on a notion of security wrappers, where a wrapper encloses an object or a component and controls its interactions with the environment. Our run-time system automatically adds a wrapper to an insecure component. The wrappers are invisible such that a wrapped component and its environment are not aware of it. The security policies of a wrapper are formalized based on a notion of security levels. At run-time, future components will be wrapped upon need, and objects of unsafe classes will be wrapped, using static checking to limit the number of unsafe classes and thereby reducing run-time overhead. We define an operational semantics and sketch a proof of noninterference. A service provider may use wrappers to protect its services in an insecure environment, and vice-versa: a system platform may use wrappers to protect itself from insecure service providers. Keywords: Active objects · Futures · Information-flow security · Noninterference · language-based security · Distributed systems

• Fazeldehkordi, Elahe & Owe, Olaf (2019). Futures, Histories, and Smart Contracts. Full text in Research Archive
• Fazeldehkordi, Elahe; Owe, Olaf & Ramezanifarkhani, Toktam (2019). A Language-Based Approach to Prevent DDoS Attacks in Distributed Financial Agent Systems. Full text in Research Archive
• Fazeldehkordi, Elahe; Owe, Olaf & Noll, Josef (2019). Security and Privacy Functionalities in IoT. Full text in Research Archive
• Tokas, Shukun; Owe, Olaf & Ramezanifarkhani, Toktam (2019). Language-Based Mechanisms for Privacy by Design. Full text in Research Archive Show summary

  Best Paper Award

• Karami, Farzane; Owe, Olaf; Schneider, Gerardo & Johansen, Christian (2018). The Future Mechanism and Information Flow Security. Full text in Research Archive
• Ramezanifarkhani, Toktam; Owe, Olaf & Fazeldehkordi, Elahe (2017). Security Functionality of IoT Devices. Full text in Research Archive Show summary

  in proceedings of the Ph.D. Symposium at iFM’17 on Formal Methods: Algorithms, Tools and Applications, CRIStin 1490782, 2017.

• Ramezanifarkhani, Toktam; Karami, Farzane & Owe, Olaf (2017). A High-Level Language for Active Objects with Future-Free Support of Futures. Full text in Research Archive
• Ramezanifarkhani, Toktam; Fazeldehkordi, Elahe & Owe, Olaf (2017). A Language-Based Approach to Prevent DDoS Attacks in Distributed Object Systems. Full text in Research Archive
• Tokas, Shukun; Owe, Olaf & Johansen, Christian (2017). Code Diversification Mechanisms for Securing the Internet of Things. Full text in Research Archive
• Ramezanifarkhani, Toktam & Owe, Olaf (2016). A Secrecy-Preserving Language for Programming of Object-Oriented and Distributed Systems. Full text in Research Archive
• Owe, Olaf; Lin, Jia-Chun & Yu, Ingrid Chieh (2015). A Formal Framework Supporting Unrestricted Software Changes in Object-Oriented Concurrent Systems. Full text in Research Archive
• McDowell, Charlie & Owe, Olaf (2015). Flooding Detection in Concurrent Object Systems. Full text in Research Archive
• Owe, Olaf; Steffen, Martin & Telle, Jan Arne (2013). The 18th International Symposium on Fundamentals of Computation Theory. Information and Computation. ISSN 0890-5401. 231, p. 1–2. doi: 10.1016/j.ic.2013.08.001. Full text in Research Archive
• Din, Crystal Chang; Bubel, Richard & Owe, Olaf (2013). Comparison of Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. In proceedings of NWPT'13. Full text in Research Archive
• Owe, Olaf; Telle, Jan Arne & Steffen, Martin (2011). Preface to the Proceedings of the 18th International Symposium in Fundamentals of Computation Theory FCT 2011. In Owe, Olaf; Steffen, Martin & Telle, Jan Arne (Ed.), Fundamentals of Computation Theory - 18th International Symposium, FCT 2011, Oslo, Norway, August 22-25, 2011. Springer. ISSN 9783642229534. Full text in Research Archive
• 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.

• Ramezanifarkhani, Toktam; Karami, Farzane; Owe, Olaf & Steffen, Martin (2023). Language-based Approaches for Enforcing Privacy and Security Policies. Universitetet i Oslo. Full text in Research Archive Show summary

  Nowadays, compliance with the General Data Protection Regulation (GDPR) poses a significant challenge for enterprises processing personal data. The GDPR protects individuals' privacy and imposes strict requirements on the processing of such data. Failure to comply with the GDPR can result in fines of up to 20 million Euros or even 4% of the company's total annual turnover. In this thesis, Farzane Karami has focused on exploring methods to enforce the GDPR requirements at the level of a programming language. Karami’s approach involves designing an object-oriented programming language that enforces the GDPR's data usage requirements during program execution. The contributions of this thesis can be categorized as follows: 1) Designing a data protection language (called DPL) with the necessary language features to enforce the GDPR requirements, 2) Formalizing and simulating DPL’s semantics in a logical framework, which provides an executable interpreter to experiment and verify that DPL programs cannot violate the GDPR properties 3) Providing a pen and paper proof to verify our claims. In this thesis, we also conduct research on enforcing security policies in distributed systems, where only authorized entities can access confidential data. We use the language-based approaches and formal methods to automate program analysis and verify whether a program is secure.

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

• Ramezanifarkhani, Toktam; Okafor, Lara & Owe, Olaf (2022). Security for marginalized people. (Digital (in) security: safety for queer people of color in a digitalized world). Faculty of Mathematics and Natural Sciences, UiO. Full text in Research Archive
• Ramezanifarkhani, Toktam; Owe, Olaf; Steffen, Martin & Tokas, Shukun (2021). Analysis and Enforcement of GDPR-related Privacy Principles in Object-Oriented Distributed Systems. Universitetet i Oslo. Full text in Research Archive Show summary

  Privacy is recognized as a fundamental human right in the European Union, giving the right to a private life and associated freedom. In the midst of digital disruption, to have a meaningful balance between the fundamental privacy rights, innovation, and economic growth, it is therefore important to consider privacy as a primary requirement in system engineering. This thesis provides fundamental computing concepts for privacy, in order to facilitate construction of privacy-compliant systems. By making privacy as an intrinsic component in design and development of systems, contributions of this thesis provide a way to turn privacy needs into tangible controls and a way to verify if the system is privacy compliant. In particular, the thesis focus on GDPR’s specific privacy requirements: data protection by design and data subject access request. There is a growing demand for verifiable privacy compliance in order to produce evidence for regulatory requirements such as accountability, transparency, etc. And this research work is at the intersection of GDPR-related privacy requirements and formal methods to facilitate a formal specification and verification of privacy compliance.

• Ramezanifarkhani, Toktam; Fazeldehkordi, Elahe; Owe, Olaf; Noll, Josef & Johansen, Christian (2021). Security and Privacy Solutions in IoT and Distributed Systems Design. Universitetet i Oslo. Full text in Research Archive Show summary

  The ground beneath our feet is anything but dry; there is more water held in Earth’s rocks than all the world’s oceans combined. Fluids in the subsurface are always on the move and understanding this is important in the fields of hydrocarbon exploration, CO2 storage and hydrogeology. Pore pressure is the pressure of fluids found within rock pore spaces and is the principal driver of subsurface fluid movement. Abnormally high pore pressures are a well-documented phenomenon throughout the world, whereas abnormally low pore pressures are rare and poorly understood. The northern Barents shelf provides a globally unique example of the latter, where extremely low pore pressures are observed offshore and onshore. The candidate’s PhD research shows that all cases of abnormally low pressure have undergone geologically recent uplift and typically occur at relatively shallow depths. In the Barents shelf, including the High Arctic Svalbard archipelago, low pressures must have developed in the last few thousand years and are in a present state of disequilibrium. Indeed, this disequilibrium has probably driven geologically recent fluid migration and is almost certainly still happening today.

• Pun, Violet Ka I; Stolz, Volker; Fazeldehkordi, Elahe; Owe, Olaf; Ramezanifarkhani, Toktam & Damasceno, Carlos Diego Nascimento [Show all 13 contributors for this article] (2020). Proceedings of the PhD Symposium at iFM’19on Formal Methods: Algorithms, Tools and Applications (PhD-iFM’19). Høgskulen på Vestlandet. ISSN 9788293677345. Full text in Research Archive Show summary

  Preface: This research report contains the proceedings of the PhD Symposium at iFM’19 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM’19), which was held on 3 December, 2019 at Western Norway University of Applied Sciences, Bergen, Norway. The program of the symposium consisted of an invited talk by Andreas Griesmayer (ARM, Cambridge, UK) and 11 short presentations. Each short presentation received advices and feedbacks from a senior researcher. Among the 11 short presentations, 5 submitted their contributions in the form of extended abstracts, which were included in this report.

• Tokas, Shukun; Owe, Olaf & Johansen, Christian (2020). Code Diversification Mechanisms for Internet of Things (Revised Version 2). Universitetet i Oslo. ISSN 9788273684387. Full text in Research Archive
• Lee, Ming-Chang & Owe, Olaf (2016). Semantic Modeling of Smart Homes in the ABS Real-time modeling language. Department of Informatics, University of Oslo. ISSN 9788273684226. Full text in Research Archive
• Din, Crystal Chang & Owe, Olaf (2014). Compositional and sound seasoning about active objects with shared futures. Universitetet i Oslo. Full text in Research Archive Show summary

  Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. The future mechanism extends the traditional method call communication model by facilitating sharing of references to futures. By assigning method call result values to futures, third party objects may pick up these values. This may reduce the time spent waiting for replies in a distributed environment. However, futures add a level of complexity to program analysis, as the program semantics becomes more involved. This paper presents a model for asynchronously communicating objects, where return values from method calls are handled by futures. The model facilitates invariant specifications over the locally visible communication history of each object. Compositional reasoning is supported and proved sound, as each object may be specified and verified independently of its environment. A kernel object-oriented language with futures inspired by the ABS modeling language is considered. A compositional proof system for this language is presented, formulated within dynamic logic.

• Din, Crystal Chang; Owe, Olaf & Bubel, Richard (2013). A comparison of runtime assertion checking and theorem proving for concurrent and distributed systems. Universitetet i Oslo. Full text in Research Archive Show summary

  We investigate the usage of a history-based specification approach for concurrent and distributed systems. In particular, we compare two approaches on checking that those systems behave according to their specification. Concretely, we apply runtime assertion checking and static deductive verification on two small case studies to detect specification violations, respectively to ensure that the system follows its specifications. We evaluate and compare both approaches with respect to their scope and ease of application. We give recommendations on which approach is suitable for which purpose as well as the implied costs and benefits of each approach.

• Din, Crystal Chang; Dovland, Johan & Owe, Olaf (2012). An approach to compositional reasoning about concurrent objects and futures. Universitetet i Oslo. Full text in Research Archive Show summary

  Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. Rather than performing analysis at the code level of mainstream objectoriented languages such as Java and C++, we consider an imperative, objectoriented language with a simpler concurrency model. This language, based on concurrent objects communicating by asynchronous method calls and futures, avoids some difficulties of mainstream object-oriented programming languages related to compositionality and aliasing. In particular, reasoning about futures is handled by means of histories. Compositional verification systems facilitate system analysis, allowing components to be analyzed independently of their environment. In this paper, a compositional proof system in dynamic logic for partial correctness is established based on communication histories and class invariants. The soundness and relative completeness of this proof system follow by construction using a transformational approach from a sequential language with a non-deterministic assignment operator.

• Johansen, Christian & Owe, Olaf (2012). Dynamic Structural Operational Semantics (preliminary version). Universitetet i Oslo. Full text in Research Archive Show summary

  We introduce Dynamic SOS as a framework for describing semantics of programming languages that include dynamic software upgrades. Dynamic SOS is built on top of theModular SOS of P.Mosses, with an underlying category theory formalization. Dynamic SOS wants to bring out the essential differences between dynamic upgrade constructs and execution constructs. The important feature of Modular SOS that we exploit in our framework is the sharp separation of the program code from the additional data structures needed at run-time. We exemplify Dynamic SOS on the C-like Proteus language and the concurrent object-oriented Creol language. On the way we introduce a construction onModular SOS useful in the setting of the concurrent objects of Creol, where the executing code is running inside the object. This “encapsulating construction” may be used in any situation where a form of encapsulation of the execution is needed.

• Din, Crystal Chang; Dovland, John; Johnsen, Einar Broch & Owe, Olaf (2010). Observable behavior of distributed systems : component reasoning for concurrent objects. Universitetet i Oslo. Full text in Research Archive Show summary

  We present a partial correctness proof system for ABS, an imperative, concurrent and object-oriented language which provides asynchronous communication model that is suitable for loosely coupled objects in the distributed setting. The proof system is derived from a standard sequential language by means of a syntactic encoding and applies Hoare rules. The execution of a distributed system is represented by its communication history, which can be predicated by history invariant. Modularity is achieved by establishing history invariants independently for each object and composed at need. This results in behavioral specification of distributed system in an open environment. As a case study we model and analyze the reader-writer example in the framework we developed.

• Bentea, Lucian & Owe, Olaf (2010). Towards an object-oriented modeling language for probabalistic open distributed systems. Universitetet i Oslo. Full text in Research Archive Show summary

  In this paper, we propose a probabilistic extension of the Creol modeling language, called PCreol, for which we give the operational semantics in Probabilistic Rewrite Logic. We give details on the implementation of a prototype PCreol interpreter, executable in Maude, on top of the existing one for Creol. We also achieved the integration of PCreol with the VeStA tool, which allows for statistical model checking and statistical quantitative analysis of PCreol programs. We give two example PCreol programs and show how VeStA can be used to study their properties. The paper is concluded with a number of future research directions.

View all works in NVA