Verifying a Real-Time Language with Constraints

Formal verification of real time programs, where variables can be assigned different values at every single time, is difficult due to the analyses of loops with time lags. In this paper, we consider a problem arising from verification of real-time languages: checking of the range of stream variables. We propose a constraint model for this problem, and an algorithm, combining constraint propagation and an ad hoc solving method, for solving it. We apply our method to the FAUST language, a language for processing audio streams. Experiments show that our approach provides very good results in short times.