--- abstract: "In this paper we describe the successful application of the ProB validation\r\ntool on an industrial case study. The case study centres on the\r\nSan Juan metro system installed by Siemens. The control software was\r\ndeveloped and formally proven with B. However, the development contains\r\ncertain assumptions about the actual rail network topology which\r\nhave to be validated separately in order to ensure safe operation.\r\nFor this task, Siemens has developed custom proof rules for\r\nAtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory).\r\nThese properties thus had to be validated by hand at great expense (and they need to be\r\nrevalidated whenever the rail network infrastructure changes).\r\n\r\nIn this paper we show how we were able to use ProB to validate all of the\r\nabout 300 properties of the San Juan deployment, detecting exactly the\r\nsame faults automatically in around 17 minutes that were manually uncovered in about one man-month.\r\nThis achievement required the extension of the ProB kernel for large sets\r\nas well as an improved constraint propagation phase.\r\nWe also outline some of the effort and features that were required in moving\r\nfrom a tool capable of dealing with medium-sized examples towards a tool\r\nable to deal with actual industrial specifications. Notably, a new parser and\r\ntype checker had to be developed.\r\nWe also touch upon the issue of validating ProB, so that it can\r\nbe integrated into the SIL4 development chain at Siemens." accompaniment: [] book_title: Proceedings FM 2009 commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - leuschel@cs.uni-duesseldorf.de - jerome.falampin@siemens.com - ~ - plagge@cs.uni-duesseldorf.de creators_name: - family: Leuschel given: Michael honourific: '' lineage: '' - family: Falampin given: Jérôme honourific: '' lineage: '' - family: Fabian given: Fritz honourific: '' lineage: '' - family: Daniel given: Plagge honourific: '' lineage: '' data_type: ~ date: ~ date_type: ~ datestamp: 2009-09-09 08:05:36 department: ~ dir: disk0/00/00/01/49 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 149 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/149/1/siemens_fm09_final.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: inpress issn: ~ item_issues_comment: [] item_issues_count: 0 item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2010-04-19 15:05:57 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: ~ output_media: ~ pagerange: ~ pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: ~ producers_id: [] producers_name: [] projects: [] publication: ~ publisher: Springer-Verlag refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 21 series: ~ skill_areas: [] source: ~ status_changed: 2009-09-09 08:05:36 subjects: - deploy_tooldev_modela - deploy_method_proof - deploy_industrial_trans succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Automated Property Verification for Large Scale B Models type: book_section userid: 12 volume: ~