Logic-based Schedulability Analysis for Compositional Hard Real-Time Embedded Systems
Ref: CISTER-TR-131201 Publication Date: 3, Dec, 2013
Logic-based Schedulability Analysis for Compositional Hard Real-Time Embedded SystemsRef: CISTER-TR-131201 Publication Date: 3, Dec, 2013
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.
6th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems (CRTS 2013).
Notes: Co-located within the IEEE Real-Time Systems Symposium (RTSS'13).