@conference {PintoJS:logbsachrts,
	title = {Logic-based Schedulability Analysis for Compositional Hard Real-Time Embedded Systems},
	booktitle = {6th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems - CRTS},
	year = {2013},
	month = {December},
	address = {Vancouver, Canada},
	abstract = {<p>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 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.
</p>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/jsp/files/crts2013.pdf},
	author = {Andr{\'e} Matos Pedro and David Pereira and Lu{\'\i}s Miguel Pinho and Jorge Sousa Pinto},
	editor = {Moris Behnam and Giorgio Buttazzo}
}