creators_name: Leuschel, Michael
creators_name: Falampin, Jérôme
creators_name: Fabian, Fritz
creators_name: Daniel, Plagge
creators_id: leuschel@cs.uni-duesseldorf.de
creators_id: jerome.falampin@siemens.com
creators_id: plagge@cs.uni-duesseldorf.de
type: book_section
datestamp: 2009-09-09 08:05:36
lastmod: 2010-04-19 15:05:57
metadata_visibility: show
title: Automated Property Verification for Large Scale B Models
ispublished: inpress
subjects: deploy_tooldev_modela
subjects: deploy_method_proof
subjects: deploy_industrial_trans
full_text_status: public
abstract: In this paper we describe the successful application of the ProB validation
tool on an industrial case study. The case study centres on the
San Juan metro system installed by Siemens. The control software was
developed and formally proven with B. However, the development contains
certain assumptions about the actual rail network topology which
have to be validated separately in order to ensure safe operation.
For this task, Siemens has developed custom proof rules for
AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment  (running out of memory).
These properties thus had to be validated by hand at great expense (and they need to be
revalidated whenever the rail network infrastructure changes).

In this paper we show how we were able to use ProB to validate all of the
about 300 properties of the San Juan deployment, detecting exactly the
same faults automatically in around 17 minutes that were manually uncovered in about one man-month.
This achievement required the extension of the ProB kernel for large sets
as well as an improved constraint propagation phase.
We also outline some of the effort and features that were required in moving
from a tool capable of dealing with medium-sized examples towards a tool
able to deal with actual industrial specifications. Notably, a new parser and
type checker had to be developed.
We also touch upon the issue of validating ProB, so that it can
be integrated into the SIL4 development chain at Siemens.
publisher: Springer-Verlag
refereed: TRUE
book_title: Proceedings FM 2009
citation:   Leuschel, Michael and Falampin, Jérôme and Fabian, Fritz and Daniel, Plagge   Automated Property Verification for Large Scale B Models.   In:  Proceedings FM 2009.   Springer-Verlag.     (In Press)  
document_url: http://deploy-eprints.ecs.soton.ac.uk/149/1/siemens_fm09_final.pdf