Determining robustness of synchronous programs under stuttering

Abstract

Robustness of embedded systems under potential changes in their environment is crucial for reliable behaviour. One typical environmental impact is that of the inputs being slowed down — due to which, the system may no longer satisfy its specification. In this paper, we present a framework for analysing the behaviour of synchronous programs written in Lustre under such environmental interference. Representing slow input by stuttering, we introduce both strong and weak slowdown

robustness constraints with respect to this phenomenon. Furthermore, static and dynamic algorithmic techniques are used to

deduce whether such constraints are satisfied, and the relationship between stateful programs and the slowdown model considered is explored.