Browsing HVL Open by Author "Johnsen, Einar Broch"

Now showing items 1-7 of 7

    • Active Objects with Deterministic Behaviour 

      Ka I Pun, Violet; Henrio, Ludovic; Johnsen, Einar Broch (HVL-Rapport;8/2020, Report, 2020)
      Active objects extend the Actor paradigm with structured communication using method calls and futures. Active objects are, like actors, known to be data race free. Both are inherently concurrent, as they share a fundamental ...

    • Analysis of SLA Compliance in the Cloud -- An Automated, Model-based Approach 

      de Boer, Frank; Giachino, Elena; de Gouw, Stijn; Hähnle, Reiner; Johnsen, Einar Broch; Laneve, Cosimo; Pun, Ka I; Zavattaro, Gianluigi (Peer reviewed; Journal article, 2019)
      Service Level Agreements (SLA) are commonly used to specify the quality attributes between cloud service providers and the customers. A violation of SLAs can result in high penalties. To allow the analysis of SLA compliance ...

    • From SOS to asynchronously communicating actors 

      de Boer, Frank; Johnsen, Einar Broch; Pun, Ka I; Tapia Tarifa, Silvia Lizeth (Peer reviewed; Journal article, 2020)
      Structural Operational Semantics (SOS) provides a general format to describe a model as a transition system with very powerful synchronization mechanisms. Actor systems are distributed, asynchronously communicating units ...

    • Implementing SOS with Active Objects: A Case Study of a Multicore Memory System 

      Bezirgiannis, Nikolaos; de Boer, Frank; Johnsen, Einar Broch; Pun, Ka I; Tapia Tarifa, Silvia Lizeth (Journal article; Peer reviewed, 2019)
      This paper describes the development of a parallel simulator of a multicore memory system from a model formalized as a structural operational semantics (SOS). Our implementation uses the Abstract Behavioral Specification ...

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

    • SymPaths: Symbolic Execution Meets Partial Order Reduction 

      de Boer, Frank; Bonsangue, Marcello; Johnsen, Einar Broch; Pun, Ka I; Tapia Tarifa, Silvia Lizeth; Tveito, Lars (Peer reviewed; Journal article, 2020)
      Symbolic execution is an important technique for software analysis, which enables systematic model exploration by following all possible execution paths for a given program. For multithreaded shared variable programs, this ...

    • Using coloured Petri nets for resource analysis of active objects 

      Gkolfi, Anastasia; Johnsen, Einar Broch; Kristensen, Lars Michael; Yu, Ingrid Chieh (Journal article; Peer reviewed, 2018)
      Pay-on-demand resource provisioning is an important driver for cloud computing. Virtualized resources in cloud computing open for resource awareness, such that applications may contain resource management strategies to ...