The notations are often too difficult to learn and use, do not provide adequate tool support, do not integrate well into the software development process or are too difficult for users to interpret. Our aim is to make formal behaviour models and the benefits of analysis accessible to mere software engineering mortals. Experience has shown that scenario-based requirements specification and behaviour animation are useful explanatory techniques, appreciated by users. In this talk we outline our attempt to facilitate the development of behaviour models in conjunction with scenarios. Analysis can then be performed by compositional reachability analysis using the LTSA analyzer.
Animation is used to help explain both model behaviour and misbehaviour to users.