Logic-based schedulability analysis for compositional hard real-time embedded systems

Pedro, André; Pereira, David; Pinho, Luís Miguel; Pinto, Jorge Sousa

http://hdl.handle.net/10400.22/6816

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
ART_CISTER_2015_matos_pedro.pdf		1.03 MB	Adobe PDF	Download

Send Feedback

Authors

Abstract(s)

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.