Internship Proposal (M2): Sensitivity Analysis in Timed Automata

Timed systems refer to computer systems in which timing information plays a crucial role. The correctness of such system rely not only on functional correctness (i.e. computing the right value), but also on extra-functional properties such as response time and worst-case execution time. Embedded systems, such as controllers found in cars, are examples of timed systems. Several methods exist for modeling and verifying different aspects of such systems [1]. One difficulty that arises with timed systems is that they can lack predictability; for instance, task execution times can vary due to different factors including imprecise clocks and unexpected resource usage. Sensitivity analysis addresses this issue [3]: given a nominal model that captures the behaviors of the system in an idealistic setting, one analyzes the behaviors of the system when its parameters are subject to perturbations. In this internship, we concentrate on perturbations on timing constraints in systems modeled by timed automata [2]. Given a timed automaton that models the nominal behaviors, we consider the executions of the model where each duration is subject to random noise. Given a specification expressed in a timed logic [5] or using timed automata [2], we would like to quantify the sensitivity of the system. Some starting questions for which we will seek answers are the following. 1. Given n and > 0, what is the probability of the perturbed executions to have a distance of more than t