<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>10</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Jorge Sousa Pinto</style></author><author><style face="normal" font="default" size="100%">André Matos Pedro</style></author><author><style face="normal" font="default" size="100%">David Pereira</style></author><author><style face="normal" font="default" size="100%">Luís Miguel Pinho</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Logic-based schedulability analysis for compositional hard real-time embedded systems</style></title></titles><dates><year><style  face="normal" font="default" size="100%">2015</style></year></dates><abstract><style face="normal" font="default" size="100%">&lt;p&gt;Over the past decades several approaches for schedu- lability analysis have been proposed for both uniprocessor 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 misinterpretations 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 uniprocessor 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.&lt;/p&gt;
</style></abstract></record></records></xml>