%T Schedulability Analysis of Timed CSP Models Using the PAT Model Checker
%A Oguzcan Oguz, Jan F. Broenink, Angelika Mader
%E Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2012
%X Timed CSP can be used to model and analyse real\-time and
concurrent behaviour of embedded control systems. Practical
CSP implementations combine the CSP model of a real\-time
control system with prioritized scheduling to achieve
efficient and orderly use of limited
resources. Schedulability analysis of a timed CSP model of a
system with respect to a scheduling scheme and a particular
execution platform is important to ensure that the system
design satisfies its timing requirements. In this paper, we
propose a framework to analyse schedulability of CSP\-based
designs for non\-preemptive fixed\-priority
multiprocessor scheduling. The framework is based on the PAT
model checker and the analysis is done with dense\-time
model checking on timed CSP models. We also provide a
schedulability analysis workflow to construct and analyse,
using the proposed framework, a timed CSP model with
scheduling from an initial untimed CSP model without
scheduling. We demonstrate our schedulability analysis
workflow on a case study of control software design for a
mobile robot. The proposed approach
provides non\-pessimistic schedulability results.
If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.
Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.
Pages © WoTUG, or the indicated author. All Rights Reserved.
Comments on these web pages should be addressed to: www at wotug.org