Modeling of Real-Time System Designs for Parametric Analysis

In designing real time software, system designers need to find out the time budget to allocate to each action of real time tasks so that the tasks can meet their deadlines. Our solution to this problem involves representing the execution time of the actions as parameters, then analyzing the collaborative behavior of those real time tasks. This paper proposes parametric timed models of real time tasks whose executions are controlled by a scheduler. We develop an algorithm to synthesize a coherent model which represents the possible behavior from a set of real time tasks by exhaustively searching their reachable states. A set of linear inequalities are then derived on the fly from the synthesized model as the condition of parameters for schedulability. By solving the inequalities using a constraint solver, we can obtain desirable values of the parameters. In addition, we have implemented the algorithm in a tool and conducted some experiments to show the effectiveness of our approach.