Schedulability analysis of timed CSP models using the PAT model checker

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

    34 Downloads (Pure)

    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.
    Original languageUndefined
    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
    Pages65-88
    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
    http://wotug.org/cpa2012/

    Publication series

    Name
    PublisherOpen Channel Publishing Ltd

    Conference

    ConferenceCommunicating Process Architectures, CPA 2012
    CountryUnited Kingdom
    CityDundee
    Period26/08/1229/08/12
    Internet address

    Keywords

    • METIS-289676
    • IR-83355
    • Model Checking
    • CSP
    • EWI-22198
    • Real time systems
    • Schedulability analysis
    • Timed CSP
    • PAT

    Cite this