--- abstract: "In this paper we examine the difference between model checking high-level and low-level models.\r\nIn particular, we compare the ProB model checker for the B-method and the spin model checker for Promela.\r\nWhile 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\r\n specifications with ProB.\r\nWe investigate the reasons for this behaviour, examining expressivity, granularity and spin's search algorithms.\r\nWe also show that certain types of information (such as symmetry) can be more easily inferred and exploited in high-level\r\n models, leading to a considerable reduction in model checking time." accompaniment: [] book_title: Proceedings ABZ'2008 commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - leuschel@cs.uni-duesseldorf.de creators_name: - family: Leuschel given: Michael honourific: '' lineage: '' data_type: ~ date: 2008 date_type: published datestamp: 2008-11-04 08:57:08 department: ~ dir: disk0/00/00/00/43 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 43 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/43/1/abz08_invited.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: pub 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:51 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: http://www.springerlink.com/content/1075831680075025/ output_media: ~ pagerange: 4-23 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: ~ producers_id: [] producers_name: [] projects: [] publication: ~ publisher: Springer-Verlag refereed: FALSE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 21 series: ~ skill_areas: [] source: ~ status_changed: 2008-11-04 08:57:08 subjects: - deploy_tooldev - deploy_tooldev_modela succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: 'The High Road to Formal Validation: Model Checking High-Level versus Low-Level Specifications' type: book_section userid: 12 volume: ~