Industrial deployment of system engineering methods providing high dependability and productivity

 

The High Road to Formal Validation: Model Checking High-Level versus Low-Level Specifications

Leuschel, Michael (2008) The High Road to Formal Validation: Model Checking High-Level versus Low-Level Specifications. In: Proceedings ABZ'2008. Springer-Verlag, pp. 4-23.

[img]
Preview
PDF - Accepted Version
264Kb

Official URL: http://www.springerlink.com/content/1075831680075025/

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 high-level models, leading to a considerable reduction in model checking time.

Item Type:Book Section
Subjects:Tool developments
Tool developments > Model checking
ID Code:43
Deposited By:Prof Michael Leuschel
Deposited On:04 Nov 2008 08:57
Last Modified:19 Apr 2010 16:05

Repository Staff Only: item control page

Deploy-Project - All right reserved