Schedulability analysis of timed CSP models using the PAT model checker

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    53 Downloads (Pure)


    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.
    Original languageEnglish
    Title of host publicationCommunicating Process Architectures 2012
    EditorsP.H. Welch, F.R.M. Barnes, K. Chalmers, J.B. Pedersen, A.T. Sampson
    Place of PublicationBicester
    PublisherOpen Channel Publishing Ltd
    Number of pages24
    ISBN (Print)978-0-9565409-5-9
    Publication statusPublished - 27 Aug 2012
    EventCommunicating Process Architectures, CPA 2012: 34th WoTUG Conference on Concurrent and Parallel Programming - University of Abertay, Dundee, United Kingdom
    Duration: 26 Aug 201229 Aug 2012
    Conference number: 34


    ConferenceCommunicating Process Architectures, CPA 2012
    Country/TerritoryUnited Kingdom
    Internet address


    • Model Checking
    • CSP
    • Real time systems
    • Schedulability analysis
    • Timed CSP
    • PAT


    Dive into the research topics of 'Schedulability analysis of timed CSP models using the PAT model checker'. Together they form a unique fingerprint.

    Cite this