Visualizing graphs with a large number of edges and vertices can be cumbersome and ineffective. This is due to the presence of countless overlapping arrows, which makes a graph unclear and hard to understand and interpret by a human. The aim of this paper is to try to address this problem using a new concept of data visualization, namely pie tree visualization. We illustrate this technique on the module architecture of a real-life development from the project Deploy. We first describe pie tree visualization, and then, present its advantages.

During previous teaching and research experience, we have accumulated anecdotal evidence that using a high-level formalism such as B can be much more productive than using a low-level formalism such as Promela. Furthermore, quite surprisingly, it turned out that the use of a high-level model checker such as prob, was much more effective in practice than using a very efficient model checker such as spin on the corresponding low-level model. In this paper, we try to put this anecdotal evidence on a more firm empirical footing, by systematically comparing the development and validation of B models with the development and validation corresponding Promela models. These experiments have confirmed our previous experience, and show the merits of using a high-level specification language such as B, both in a teaching and in a research environment.