The High Road to Formal Validation:

12 years 7 months ago
The High Road to Formal Validation:
Abstract. In this paper we examine the difference between model checking high-level and low-level models. In particular, we compare the ProB model checker for the B-method and the SPIN model checker for Promela. While SPIN has a dramatically more efficient model checking engine, we show that in practice the performance can be disappointing compared to model checking high-level specifications with ProB. We investigate the reasons for this behaviour, examining expressivity, granularity and SPIN's search algorithms. We also show that certain types of information (such as symmetry) can be more easily inferred and exploited in highlevel models, leading to a considerable reduction in model checking time.
Michael Leuschel
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where ASM
Authors Michael Leuschel
Comments (0)