Specification-based testing of synchronous software

Synchronous programming makes the implementation of reactive software easier and safer. Automatic formal verification methods based on model-checking have been developed within the synchronous approach to prove the satisfaction by the software of safety properties. But these methods often require huge memory or time amounts. As a solution to that problem we propose a set of formally defined testing techniques allowing for automatic test data generation. These techniques can be used independently or as a complement to formal verification, since they need the same set of specifications.