Advisors : Mathias Ramparison, Lionel Rieg, Catherine Vigouroux
Safe timing analysis in critical systems relies on the composition of local worst cases : the global worst case of the system is built from local worst cases for each component. Unfortunately, this methodology is not sound in general, as the local worst cases do not always lead to the global one, a phenomenon called a timing anomaly.
The goal of this internship is to study under which conditions a timing anomaly may occur. To that end, we plan to use fault trees, which allow to express which combinations of elementary events trigger a given target objective. Converting the fault trees to parametric automata, we can synthesize model parameters that lead to this objective (here, a timing anomaly).
More detail is available in the attached pdf description.