RTProb -Real Time Probabilsitic Tool for Probabilistic Schedulability Analysis using Markov Chain

This paper presents a probabilistic schedulability analysis tool for probabilistic Real-Time Systems (pRTS). By pRTS we intend a real-time system in which at least one of its parameter is defined using a probability distribution; in our case this parameter is the task Worst Case Execution Time (WCET) which is the probabilistic, probabilistic WCET (pWCET). The tool implements a formalism which is based on formal methods for modelling and analysis of pRTSs. It uses pWCETs to construct Continuous Time Markov Chain models, one per task job. For each job, the CTMC describes the job execution by taking into account all the interferences (probabilistic delays) that might exist. The tool also interface with model checkers for checking the models built. The results of the analysis as given by the tool are the probability of deadline miss and the response time curves for each task and for each job of the tasks.