Animation de spécifications formelles des exigences

Spécifier déclarativement les exigences relatives à des
systèmes composites présentant des aspect temps-réel à l'aide d'un
langage formel nécessite une part de validation. Une façon d'y
parvenir est de permettre aux participants de tester les propriétés
dynamiques du système par le biais d'animation. Des
"comportements" du système et de son environement sont
progressivement créés en interaction avec un outil (appelé animateur)
qui va contrôler si ceux-ci respectent les contraintes de la spécification
au fur et à mesure qu'ils sont introduits. Notre travail se concentre sur
le développement d'un tel outil pour le langage Albert II qui soit
capable de traîter l'indéterminisme présent dans le langage, de fournir
des possibilités de backtracking "intelligent" tout en permettant
l'animation symbolique et distribuée. Notre recherche s'inscrit
également dans le cadre du projet ESPRIT LTR CREWS
(Cooperative Requirements Engineering with Scenarios) qui a
l'ambition plus grande d'étudier comment l'utilisation de scénarios (ce
que sont nos "comportements" en fait) peut améliorer l'ingénierie des
exigences de systèmes informatiques.