Compositional schedulability analysis of real-time actor-based systems

Mohammad Mahdi Jaghoori, Frank De Boer, Delphine Longuet, Tom Chothia, M Sirjani

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)
122 Downloads (Pure)

Abstract

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.
Original languageEnglish
Pages (from-to)1-36
Number of pages36
JournalActa Informatica
Early online date25 Jan 2016
DOIs
Publication statusE-pub ahead of print - 25 Jan 2016

Fingerprint

Dive into the research topics of 'Compositional schedulability analysis of real-time actor-based systems'. Together they form a unique fingerprint.

Cite this