text: Parametric analysis is a powerful tool for designing modern embedded systems, because it permits to explore the space of design parameters, and to check the robustness of the system with respect to variations of some uncontrollable variable. In this paper, we address the problem of parametric schedulability analysis of distributed real-time systems scheduled by fixed priority. In particular, we propose two different approaches to parametric analysis: the first one is a novel technique based on classical schedulability analysis, whereas the second approach is based on model checking of Parametric Timed Automata (PTA). The proposed analytic method extends existing sensitivity analysis for single processors to the case of a distributed system, supporting preemptive and non-preemptive scheduling, jitters and unconstrained deadlines. Parametric Timed Automata are used to model all possible behaviours of a distributed system, and therefore it is a necessary and sufficient analysis. Both techniques have been implemented in two software tools, and they have been compared with classical holistic analysis on two meaningful test cases. The results show that the analytic method provides results similar to classical holistic analysis in a very efficient way, whereas the PTA approach is slower but covers the entire space of solutions.
  @cite_18: The tool Imitator implements the Inverse Method (IM) for Timed Automata (TAs). Given a TA ( A ) and a tuple π 0 of reference valuations for timings, IM synthesizes a constraint around π 0 where ( A ) behaves in the same discrete manner. This provides us with a quantitative measure of robustness of the behavior of ( A ) around π 0. The new version Imitator 2.5 integrates the new features of stopwatches (in addition to standard clocks) and updates (in addition to standard clock resets), as well as powerful algorithmic improvements for state space reduction. These new features make the tool well-suited to analyze the robustness of solutions in several classes of preemptive scheduling problems.
  @cite_6: This book introduces state-of-the-art verification techniques for real time embedded systems, based on the inverse method for parametric timed automata. It reviews popular formalisms for the specification and the verification of timed concurrent systems, and in particular timed automata and several extensions such as timed automata equipped with stopwatches, linear hybrid automata and affine hybrid automata. The inverse method is introduced, and its interest for guaranteeing robustness in real time systems is shown. Then it is shown how an iteration of the inverse method can solve the good parameters problem for parametric timed automata, by computing a behavioral cartography of the system. Different extensions are proposed, in particular for hybrid systems, and for applications to scheduling problems using timed automata with stopwatches. Various examples, both from the literature and from the industry, illustrate the techniques throughout the book. In particular, we perform parametric verification of abstractions of a memory circuit sold by the chipset manufacturer ST-Microelectronics, as well as of the prospective flight control system of the next generation of spacecrafts designed by ASTRIUM Space Transportation.
summary: Also based on PTA is the approach proposed by @cite_18 . Their work is based on the Inverse Method @cite_6 and it is very general because it permits to perform analysis on any system parameter. However, this generality can be paid in terms of complexity.