Transformation Heuristics for Formal Requirements Validation by Animation

International audienceSafety critical software systems are regulated by stringent certification requirements. The use of formal methods is the part of standard recommendations in particular for higher safety integrity levels. An important issue with formal methods is the problem of the validation of requirements: do they accurately capture the stakeholder needs? While proof tools guarantee the consistency of a specification, they are of little help to check if the specification models the desired behavior. This paper addresses the problem of the validation of Event-B specifications by animation. Once the specifications have been verified using the RODIN platform, they have to be transformed in order to be animated by the Brama animator. We propose transformation heuristics in order to produce a derived animatable specification which may be non-provable, but exhibiting the same behavior as the original specification