A Formal Approach to Test the Robustness of Embedded Systems using Behaviour Analysis

Robustness is an important feature required for embedded systems. This paper presents a methodology to test robustness of such systems. We investigate system behaviour aspects. We handle two formal specifications : a nominal one which describes the system behaviour in normal conditions and a degraded one which describes the behaviour in critical conditions. Both are described as Labelled Transition Systems for the untimed systems and as Timed Automata for timed systems. We extract test sequences from the nominal or from the degraded specification. We perform fault injection on these test sequences. Finally, we submit these sequences to the Implementation Under Test (IUT) and then we analyze its behaviour using adequate robustness relations.