creators_name: Leuschel, Michael
creators_id: leuschel@cs.uni-duesseldorf.de
type: book_section
datestamp: 2008-11-04 08:57:08
lastmod: 2010-04-19 15:05:51
metadata_visibility: show
title: The High Road to Formal Validation: Model Checking High-Level versus Low-Level Specifications
ispublished: pub
subjects: deploy_tooldev
subjects: deploy_tooldev_modela
full_text_status: public
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.
date: 2008
date_type: published
publisher: Springer-Verlag
pagerange: 4-23
refereed: FALSE
book_title: Proceedings ABZ'2008
official_url: http://www.springerlink.com/content/1075831680075025/
citation:   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.      
document_url: http://deploy-eprints.ecs.soton.ac.uk/43/1/abz08_invited.pdf