Animation of formal requirements specifications

Declaratively specifying requirements on real-time composite systems
with a formal language requires validation by stakeholders. One way to
perform such validation is allowing people to experience the dynamic
properties of the system to be built by animation. Behaviours of the
system and its environment are progressively created by interacting
with a tool (called animator) which will check if they respect the
constraints of the specification as they are introduced. Our work
focuses on developping such a tool for the Albert II language provided
that the tool should be able to deal with undeterminism and make
available "intelligent" backtracking, symbolic and distributed
animation. Our research is also part of the ESPRIT LTR project
CREWS (Cooperative Requirements Engineering with Scenarios)
which has the greater ambition of studying how scenarios (what our
"behaviours" are, in fact) can help in Requirements Engineering.