Opin vísindi

Compositional schedulability analysis of real-time actor-based systems

Compositional schedulability analysis of real-time actor-based systems

Title: Compositional schedulability analysis of real-time actor-based systems
Author: Jaghoori, Mohammad Mahdi
de Boer, Frank
Longuet, Delphine
Chothia, Tom
sirjani, marjan   orcid.org/0000-0001-5478-0987
Date: 2016-01-25
Language: English
Scope: 343-378
University/Institute: Háskólinn í Reykjavík
Reykjavik University
School: Tölvunarfræðideild (HR)
School of Computer Science (RU)
Series: Acta Informatica;54(4)
ISSN: 0001-5903
1432-0525 (eISSN)
DOI: 10.1007/s00236-015-0254-x
Subject: Software engeneering; Software development; Computer systems; Verification; Modeling; Mathematical logic; Programming languages; System analysis; Time management; Hugbúnaðarverkfræði; Hugbúnaðargerð; Tölvukerfi; Prófanir; Líkanagerð; Stærðfræðileg rökfræði; Forritunarmál; Kerfisgreining; Tímastjórnun
URI: https://hdl.handle.net/20.500.11815/1589

Show full item record


Jaghoori, M. M., de Boer, F., Longuet, D., Chothia, T., & Sirjani, M. (2017). Compositional schedulability analysis of real-time actor-based systems. Acta Informatica, 54(4), 343–378. https://doi.org/10.1007/s00236-015-0254-x


We present an extension of the actor model with real-time, including deadlines associated with messages, and explicit application-level scheduling policies, e.g.,"earliest deadline first" which can be associated with individual actors. Schedulability analysis in this setting amounts to checking whether, given a scheduling policy for each actor, every task is processed within its designated deadline. To check schedulability, we introduce a compositional automata-theoretic approach, based on maximal use of model checking combined with testing. Behavioral interfaces define what an actor expects from the environment, and the deadlines for messages given these assumptions. We use model checking to verify that actors match their behavioral interfaces. We extend timed automata refinement with the notion of deadlines and use it to define compatibility of actor environments with the behavioral interfaces. Model checking of compatibility is computationally hard, so we propose a special testing process. We show that the analyses are decidable and automate the process using the Uppaal model checker.


This article is distributed under the terms of the Creative Commons Attribution 4.0 Interna-tional License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source,provide a link to the Creative Commons license, and indicate if changes were made

Files in this item

This item appears in the following Collection(s)