Parametric Real-Time System Feasibility Analysis Using Parametric Timed Automata

Ramadian, Yusi (2012) Parametric Real-Time System Feasibility Analysis Using Parametric Timed Automata. PhD thesis, University of Trento.

PDF (PhD thesis full text) - Doctoral Thesis
Available under License Creative Commons Attribution Non-commercial Share Alike.

PDF (PhD thesis presentation) - Presentation
Available under License Creative Commons Attribution Non-commercial No Derivatives.



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.

Item Type:Doctoral Thesis (PhD)
Doctoral School:Information and Communication Technology
Subjects:Area 01 - Scienze matematiche e informatiche > INF/01 INFORMATICA
Uncontrolled Keywords:Formal method, real-time system, temporal verification, scheduling verification.
Funders:Fondazione Bruno Kessler (FBK)
Repository Staff approval on:21 May 2012 14:03

Repository Staff Only: item control page