• A Diagrammatic Approach to Model Completion 

      Rabbi, Fazle; Lamo, Yngve; Yu, Ingrid Chieh; Kristensen, Lars Michael (Peer reviewed; Journal article, 2015)
    • An MDE Approach for Modelling and Reasoning about Multi-agent Systems 

      Rabbi, Fazle; Lamo, Yngve; Kristensen, Lars Michael (Journal article; Peer reviewed, 2017)
      Epistemic logic plays an important role in artificial intelligence for reasoning about multi-agent systems. Current approaches for modelling multi-agent systems with epistemic logic use Kripke semantics where the knowledge ...
    • Analysis and evaluation of conformance preserving graph transformation rules 

      Rabbi, Fazle; Lamo, Yngve; Kristensen, Lars Michael (Journal article; Peer reviewed, 2019)
      Model transformation is a formal approach for modelling the behavior of software systems. Over the past few years, graph based modeling of software systems has gained significant attention as there are numerous techniques ...
    • Application of Model-based Testing on a Quorum-based Distributed Storage 

      Wang, Rui; Kristensen, Lars Michael; Meling, Hein; Stolz, Volker (Peer reviewed; Journal article, 2017)
    • Automated test case generation for the Paxos single-decree protocol using a Coloured Petri Net model 

      Wang, Rui; Kristensen, Lars Michael; Meling, Hein; Stolz, Volker (Peer reviewed; Journal article, 2019)
      Implementing test suites for distributed software systems is a complex and time-consuming task due to the number of test cases that need to be considered in order to obtain high coverage. We show how a formal Coloured Petri ...
    • Coverage visualization and analysis of net inscriptions in coloured Petri net models 

      Ahishakiye, Faustin; Requeno Jarabo, Jose Ignacio; Kristensen, Lars Michael; Stolz, Volker (Peer reviewed; Journal article, 2023)
      High-level Petri nets such as coloured Petri nets (CPNs) are characterized by the combination of Petri nets and a high-level programming language. In CPNs and CPN Tools, the inscriptions (e.g. arc expressions and guards) ...
    • Executing Multilevel Domain-Specific Models in Maude 

      Rodríguez, Alejandro; Duran, Francisco; Rutle, Adrian; Kristensen, Lars Michael (Peer reviewed; Journal article, 2019)
      Multilevel modelling (MLM) tackles the limitation in the number of abstraction levels present in traditional modelling approaches within the model-driven software engineering (MDSE) field. One way to specify the behaviour ...
    • Fire Risk Prediction Using Cloud-based Weather Data Services 

      Strand, Ruben Dobler; Stokkenes, Sindre; Kristensen, Lars Michael; Log, Torgrim (Peer reviewed; Journal article, 2021)
      Dry and cold winter seasons result in very dry indoor conditions and have historically contributed to severe fires in the high and dense representation of wooden homes in Norway. The fire in Lærdalsøyri, January 2014, is ...
    • Formal Specification and Validation of a Data-driven Software System for Fire Risk Prediction 

      Strand, Ruben Dobler; Kristensen, Lars Michael; Petrucci, Laure (Peer reviewed; Journal article, 2022)
      Long periods of dry and cold weather conditions significantly increase fire risks for wooden buildings. Recent advances in predictive fire risk models combined with publicly available cloud-based weather data services have ...
    • Implementation and deployment evaluation of the DMAMAC protocol for wireless sensor actuator networks 

      Kumar Somappa, Admar Ajith; Øvsthus, Knut; Kristensen, Lars Michael (Peer reviewed; Journal article, 2016)
      The increased application of wireless technologies including Wireless Sensor Actuator Networks (WSAN) in industry has given rise to a plethora of protocol designs. These designs target metrics ranging from energy efficiency ...
    • MC/DC Test Cases Generation Based on BDDs 

      Ahishakiye, Faustin; Requeno Jarabo, Jose Ignacio; Kristensen, Lars Michael; Stolz, Volker (Chapter; Peer reviewed, 2021)
      We present a greedy approach to test-cases selection for single decisions to achieve MC/DC-coverage of their Boolean conditions. Our heuristics take into account “don’t care” inputs through three-valued truth values that ...
    • Model checking starvation for resource-aware active objects with coloured petri nets 

      Gkolfi, Anastasia; Johnsen, Einar Broch; Kristensen, Lars Michael; Yu, Ingrid Chieh (Peer reviewed; Journal article, 2020)
      Dynamic resource provisioning is an important driver for pay-on-demand cloud computing. Virtualized resources open for resource awareness, such that applications may use resource management strategies to modify their ...
    • Model-based software testing for distributed systems and protocols 

      Wang, Rui (Doctoral thesis, 2020)
      Society is increasingly dependent on fault-tolerant cloud-based services which rely on the correctness and reliability of advanced distributed software systems and consensus protocols. The implementations of these systems ...
    • Model-based verification of the DMAMAC protocol for real-time process control 

      Kumar Somappa, Admar Ajith; Prinz, Andreas; Kristensen, Lars Michael (Peer reviewed; Journal article, 2015)
      Medium Access Control (MAC) protocols are responsible for managing radio communication that constitute the main energy consumer in wireless sensor-actuator networks. The Dual-Mode Adaptive MAC (DMAMAC) protocol is a recently ...
    • Multi-objective Search for Model-based Testing 

      Wang, Rui; Artho, Cyrille; Kristensen, Lars Michael; Stolz, Volker (Chapter; Peer reviewed, 2020)
      This paper presents a search-based approach relying on multi-objective reinforcement learning and optimization for test case generation in model-based software testing. Our approach considers test case generation as an ...
    • Multilevel Modelling of Coloured Petri Nets 

      Tena, Alejandro Rodriguez; Rutle, Adrian; Duran, Francisco; Kristensen, Lars Michael; Macías, Fernando (Journal article; Peer reviewed, 2018)
      Coloured Petri Nets (CPNs) is a modelling language for distributed systems which has been applied in a multitude of industrial cases. The supporting tool of CPNs is currently lacking important features such as having the ...
    • On modelling and validation of the MQTT IoT protocol for M2M communication 

      Tena, Alejandro Rodriguez; Kristensen, Lars Michael; Rutle, Adrian (Journal article; Peer reviewed, 2018)
      Machine to Machine (M2M) communication and Internet of Things (IoT) are becoming still more pervasive with the increase of communicating devices used in cyber-physical environments. A prominent approach to communication ...
    • Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification 

      Simonsen, Kent Inge Fagerland; Kristensen, Lars Michael; Kindler, Ekkart (Peer reviewed; Journal article, 2015)
      PetriCode is a tool that supports automated generation of protocol software from a restricted class of Coloured Petri Nets (CPNs) called Pragmatics Annotated Coloured Petri Nets (PA-CPNs). PetriCode and PA-CPNs have been ...
    • Proceedings of the PhD Symposium at iFM’19on Formal Methods: Algorithms, Tools and Applications (PhD-iFM’19) 

      Pun, Ka I; Stolz, Volker; Fazeldehkordi, Elahe; Owe, Olaf; Ramezanifarkhani, Toktam; Damasceno, Carlos Diego Nascimento; Damasceno, Carlos Diego Nascimento; Ahishakiye, Faustin; Kristensen, Lars Michael; Tabar, Asmae Heydari; Bubel, Richard; Hähnle, Reiner; Sagemüller, Justus; Verdier, Olivier (HVL-rapport;14/2020, Report, 2020)
      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 ...
    • Transforming Platform Independent CPN Models into Code for the TinyOS Platform: A Case Study of the RPL Protocol 

      Kristensen, Lars Michael; Veiset, Vegard (Peer reviewed; Journal article, 2013)