@InProceedings{Oguz12,
  title =        "{S}chedulability {A}nalysis of {T}imed {CSP} {M}odels {U}sing the {PAT} {M}odel {C}hecker",
  author=        "Oguz,  Oguzcan and Broenink,  Jan F. and Mader,  Angelika",
  editor=        "Welch, Peter H. and Barnes,  Frederick R. M. and Chalmers,  Kevin and Pedersen,  Jan Bækgaard and Sampson,  Adam T.",
  pages =        "65--88",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2012",
  isbn=          "978-0-9565409-5-9",
  year=          "2012",
  month=         "aug",
  abstract=      "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."
}