%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.