--- abstract: "Based on 10+ years of formal modelling in industry, I advocate the use\r\nof domain theories and modelling patterns in system modelling.\r\n\r\nWhen modelling a system, one has to somehow encode some domain data \r\nstructures\r\ninto some mathematical notation (e.g., set-theory for Event-B). This\r\nencoding is not trivial, except for very simple case studies. Inlining this\r\nencoding within a model makes it difficult to read and consequently difficult\r\nto prove. It is much better to separate the encoding in a separate file\r\n(i.e., a theory) which will describe the data structure, provide operators for\r\nupdating it together with proof rules for reasoning about them. The model is\r\nthen free from clutter and can be expressed at the same level of discourse as\r\ndomain experts.\r\n\r\nI think that AI could provide significant benefits by detecting when a model\r\nis not at the correct level of discourse and contains too much encoding. This\r\ncould be detected by inspecting the model and assessing its intrinsic\r\ncomplexity. This would be particularly useful for beginners who usually have\r\ndifficulty to separate concerns.\r\n\r\nAnother use of AI is to implement refinement plans (see paper by Grov, Ireland\r\nand Llano presented at ABZ 2012). In this setting, a failing proof is\r\nanalysed with respect to some refinement patterns and the tool suggests\r\namendment to the model that would allow to fix its proof. I think that it\r\nwould be much more valuable if the refinement patterns would be in the form of\r\ngeneric models. The tool would then propose to instantiate the generic\r\npattern and suggest ways to instantiate it (e.g., provide actual parameters).\r\nThis would reuse not only the pattern but also its associated proof. The user\r\nwould only have to prove that the actual parameters fulfill the pattern\r\npre-conditions.\r\n\r\nMore generally, AI could be used to mine existing models to extract generic\r\npatterns from them. This would allow to build a library of recurring\r\npatterns. As for refinement plans, AI could also be used for guiding users\r\nwithin the library and help them select the appropriate patterns with respect\r\nto their modelling needs.\r\n\r\nIn conclusion, using both theories and generic model patterns makes models\r\nmore easy to develop, read and prove, by allowing better reuse. AI could be\r\nof great help in assisting users for making the better use of these tools." accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: [] creators_name: - family: Voisin given: Laurent honourific: '' lineage: '' data_type: ~ date: 2012-07 date_type: published datestamp: 2012-09-20 12:48:47 department: ~ dir: disk0/00/00/04/56 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 456 event_dates: 01-06.07.2012 event_location: 'Schloss Dagstuhl, Germany' event_title: AI meets Formal Software Development event_type: workshop exhibitors_id: [] exhibitors_name: [] fileinfo: /456/2.hassmallThumbnailVersion/12271.VoisinLaurent.Slides.pdf;/456/2/12271.VoisinLaurent.Slides.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: pub 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-02-18 14:59:01 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: http://drops.dagstuhl.de/opus/volltexte/2012/3731/ output_media: ~ pagerange: ~ pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: speech producers_id: [] producers_name: [] projects: - ADVANCE publication: ~ publisher: ~ refereed: FALSE referencetext: ~ related_url_type: - pub - org related_url_url: - http://www.dagstuhl.de/12271 - http://www.systerel.fr relation_type: [] relation_uri: [] rev_number: 18 series: ~ skill_areas: [] source: ~ status_changed: 2012-09-20 12:48:47 subjects: - ADVANCE - Refinement - deploy_method_proof - theory succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: More Abstraction type: conference_item userid: 106 volume: ~