A synchronous program behaves as follows: the time is divided in discreet instants defined by a global clock. At instant t the synchronous program reads its inputs from its external environment. Then, it computes and issues outputs ot. The synchrony hypothesis presents that the computation of the output values is made instantaneously, at the same instant t. This hypothesis is satisfied when software is able to take into account any external evolution. Hence, an interactive application can be considered as a synchronous program as long as all user initiated actions and all external stimuli can be caught.

The approach is based on the Lutess testing environment. Lutess is a testing environment for functional testing of synchronous software. Lutess supports the automatic generation of input sequences for a program with respect to some environment constraints of the program under test. The environment constraints correspond to assumptions on the possible behaviours of the program environment. Input data are dynamically computed to take into account the inputs and outputs that have been produced.