Visualization of Promela with NS-Chart
Arin Chawanothai, Wiwat Vatanawood · 2019
In the paradigm of model checking, a formal model is considered as one of the crucial sources that tends to be verified with the desired properties. The definition of the formal model should be understandable and clear in order to express the structure and behaviors of the system visually using diagrammatic tools. In this paper, we focused on the formal model which is written in Promela language that supports the non-determinism of the concurrent system. From our study, we found that the Promela syntax could probably be drawn by using NS-chart visual symbols. The classic NS-chart symbols represents the control flow of the system that was written in Promela. As a main purpose of this paper, we aim to propose a set of mapping rules for generating the NS-chart drawing from Promela source codes. The result of the drawing with the proposed NS-Chart syntax showed that the Promela control flow structure could be represented succinctly and the chart could be practically used for tracing the counterexample of the verification.