A Generic Flash-Based Animation Engine for ProB

Abstract. Writing a formal specification for real-life, industrial problems is a difficult and error prone task, even for experts in formal methods. In the process of specifying a formal model for later refinement and implementation it is crucial to get approval and feedback from domain experts to avoid the costs of changing a specification at a late point of the development. But understanding formal models written in a specification language like B requires mathematical knowledge a domain expert might not have. In this paper we present a new tool to visualize B Machines using the ProB animator and Macromedia Flash. Our tool offers an easy way for specifiers to build a domain specific visualization that can be used by domain experts to check whether a B specification corresponds to their expectations.

• Type: Conference
• Year: 2007
• Where: B
• Authors: Jens Bendisposto, Michael Leuschel
• Keywords: B 2007, Domain Experts, Error Prone Task, Formal Models, Software Engineering