Parametric Real-Time System Feasibility Analysis Using Parametric Timed Automata

Real-time applications are playing an increasingly significant role in our life. The cost and risk involved in their design leads to the need for a correct and robust modelling of the system before its deployment. Many approaches have been proposed to verify the schedulability of real-time task system. A frequent limitation is that they force the task activation to restrictive patterns (e.g. periodic). Furthermore, the type of analysis carried out by the real-time scheduling theory relies on restrictive assumptions that could make the designers miss important optimization opportunities. On the other hand, the application of formal methods for verification of timed systems typically produces a yes/no answer that does not suggest any correction action or robustness margins of a given design. This work proposes an approach to combine the benefits of formal method in terms of flexibility with the production of a clear feedback for the designers. The key idea is to use parametric timed automata to enable the definition of flexible task activation patterns. The Parametric Verification of Temporal Properties (PTVP) algorithm proposed in this work produces a region of feasible parameters for realtime system. All the parameter valuation within this region is guaranteed to make the system respect the desired temporal behaviour. In this way developers are provided with a richer information than the simple feasibility of a given design choice. This method uses symbolic model checking technique to produce the result that is a union of polyhedral regions in the parameter space associated with feasible parameters. It is implemented in the tool Quinq that is based on NuSMV3. The tool also implemented an optimization to speed up the search, such as using non-parametric model checker to find counterexamples (i.e. traces) related to the unfeasible choices of parameters. Two applications of the tool and of the underlying method to several real-time system examples are presented in this dissertation : periodic real-time system tasks with offset and heterogeneous distributed real-time systems. A work that applies the tool in collaboration with another real-time system analysis tool, Modular Performance Analysis Toolbox, is also presented to show one of the many possible application of the method presented in this work. In this work we also compare our approach to the state of the art in the field of sensitivity analysis of real-time systems. However, compared to the other tools and approaches in this field, the method offered in this work presents unique advantages in the generality of the system modelling approach and the possibility to analyse the entire region of feasibility of any desired parameter in the system.