Test de spécifications de logiciels synchrones
Cet article présente une approche de vérification et de validation par le test pour les
logiciels synchrones spécifiés en Lustre. Cette approche a donné naissance à l’environnement
de test fonctionnel Lutess. Lutess comporte des outils de test fondés sur des techniques de
construction automatique de simulateurs aléatoires des spécifications du logiciel synchrone.
Dans leur version la plus simple, ces simulateurs se contentent de reproduire aléatoirement,
et de manière équiprobable, l’ensemble des comportements de l’environnement du logiciel.
Ils peuvent également être spécialisés pour favoriser l’apparition de certains comportements.
Nous présentons les fondements de l’approche et nous définissons formellement les
techniques de test sur des machines d’états finis construites à partir des spécifications.
In this paper we propose an approach for the verification and the validation of
synchronous software specified by means of the Lustre language. From this approach is born
Lutess, a functional testing environment. Lutess implements techniques making possible to
automatically build random simulators from the specifications of a synchronous software. The
basic simulation mode consists in randomly producing, with the same probability, the
behaviors of the software environment. More sophisticated modes are also provided in order
to enhance the occurrence probability of specific behaviors. We present the foundations of
our approach and we formally define the testing techniques on finite state machines built from
the software specifications.
I.PARISSIS
logiciels synchrones, lustre, validation, test à partir de spécifications.
Synchronous software, Lustre, software validation, specification-based testing.
Français
|
