Industrial deployment of system engineering methods providing high dependability and productivity


Easy Graphical Animation and Formula Visualisation for Teaching B

Leuschel, Michael and Samia, Mireille and Bendisposto, Jens and Samia, Mireille (2008) Easy Graphical Animation and Formula Visualisation for Teaching B. In: The B Method : From Research to Teaching, June 16, 2008, Nantes, France.

PDF - Accepted Version


ProB is being used for teaching the B-method. In this paper, we present two new features of ProB that we have introduced while teaching B. One feature allows a student (or an expert user) to graphically visualise any predicate as a tree. The underlying algorithm can deal with undefined subformulas and tries to provide useful feedback even for existentially quantified formulas which are false. This feature is especially useful to inspect unexpected invariant violations or operations which are unexpectedly enabled or disabled. The other feature enables a student or lecturer to easily and quickly write custom graphical state representations, to provide a better understanding of the model. With this method, one simply has to assemble a series of pictures and to write an animation function in B itself, which stipulates which pictures should be shown where depending on the current state of the model. As an additional side-benefit, writing the animation function in B itself is a good exercise for students.

Item Type:Conference or Workshop Item (Paper)
Subjects:Tool developments
Tool developments > Model checking
ID Code:47
Deposited By:Prof Michael Leuschel
Deposited On:04 Nov 2008 09:22
Last Modified:19 Apr 2010 16:05

Repository Staff Only: item control page

Deploy-Project - All right reserved