Paper Details

Communicating Process Architectures (CPA)
 Title: Schedulability Analysis of Timed CSP Models Using the PAT Model Checker
 Conference: Communicating Process Architectures 2012
 Authors: Oguzcan Oguza, Jan F. Broeninka, Angelika Maderb
(a) Robotics and Mechatronics, CTIT Institute, University of Twente
(b) Research Group Human Media Interaction (HMI), University of Twente
 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. 

BibTeX Entry

Full paper