--- abstract: "The complexity of requirements and complexity of operating environments make error detection in early stages of software system development difficult. This paper makes an argument for the use of formal modelling and verification in early stages of system development to identify and eliminate errors in a timely fashion.\r\nPrecision is key to eliminating errors in requirements while abstraction is key to mastering requirements complexity. The paper outlines the way in which precision and abstraction may be achieved through modelling and how refinement allows the complexity to be managed through layering. The role of model validation and model verification in improving the quality of formal models and in improving the quality of the requirements is also outlined. The formalism used throughout is Event-B supported by the Rodin toolset.\r\n\r\nBased on lectures given at 2012 Marktoberdorf International Summer School on Engineering Dependable Software Systems\r\n" accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - mjb@ecs.soton.ac.uk creators_name: - family: Butler given: Michael honourific: '' lineage: '' data_type: ~ date: 2012-12-06 date_type: submitted datestamp: 2012-12-06 09:51:10 department: ~ dir: disk0/00/00/04/59 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 459 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: /459/14.hassmallThumbnailVersion/Butler.pdf;/459/14/Butler.pdf|/459/2.hassmallThumbnailVersion/slides-butler.pdf;/459/2/slides-butler.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: submitted issn: ~ item_issues_comment: [] item_issues_count: ~ 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: 2013-03-09 12:50:56 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: ~ refereed: ~ referencetext: ~ related_url_type: [] related_url_url: - http://asimod.in.tum.de/2012/index.shtml relation_type: [] relation_uri: [] rev_number: 25 series: ~ skill_areas: [] source: ~ status_changed: 2012-12-06 09:51:10 subjects: - ADVANCE - deploy_training succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: Lectures given at 2012 Marktoberdorf International Summer School on Engineering Dependable Software Systems thesis_type: ~ title: Mastering System Analysis and Design through Abstraction and Refinement type: teaching_resource userid: 1 volume: ~