Compositional schedulability analysis of real-time actor-based systems

International audienceWe present an extension of the actor model with real-time, including deadlinesassociated with messages, and explicit application-level scheduling policies, e.g.,“earliestdeadline first” which can be associated with individual actors. Schedulability analysis in thissetting amounts to checking whether, given a scheduling policy for each actor, every task isprocessed within its designated deadline. To check schedulability, we introduce a compositionalautomata-theoretic approach, based on maximal use of model checking combinedwith testing. Behavioral interfaces definewhat an actor expects from the environment, and thedeadlines for messages given these assumptions.We use model checking to verify that actorsmatch their behavioral interfaces. We extend timed automata refinement with the notion ofdeadlines and use it to define compatibility of actor environments with the behavioral interfaces.Model checking of compatibility is computationally hard, so we propose a specialtesting process. We show that the analyses are decidable and automate the process using theUppaal model checker