Logic-based schedulability analysis for compositional hard real-time embedded systems
Ref: CISTER-TR-150411 Publication Date: Feb 2015
Logic-based schedulability analysis for compositional hard real-time embedded systemsRef: CISTER-TR-150411 Publication Date: Feb 2015
Over the past decades several approaches for schedulability analysis have been proposed for both uni-processor and multi-processor real-time systems. Although different techniques are employed, very little has been put forward in using formal specifications, with the consequent possibility for mis-interpretations or ambiguities in the problem statement. Using a logic based approach to schedulability analysis in the design of hard real-time systems eases the synthesis of correct-by-construction procedures for both static and dynamic verification processes. In this paper we propose a novel approach to schedulability analysis based on a timed temporal logic with time durations. Our approach subsumes classical methods for uni-processor scheduling analysis over compositional resource models by providing the developer with counter-examples, and by ruling out schedules that cause unsafe violations on the system. We also provide an example showing the effectiveness of our proposal.
Published in SIGBED Review (SIGBED Rev.), ACM, Volume 12, Issue 1, pp 56-64.