creators_name: Edmunds, Andrew creators_name: Rezazadeh, Abdolbaghi creators_name: Butler, Michael type: conference_item datestamp: 2012-03-15 09:45:21 lastmod: 2012-09-11 18:39:18 metadata_visibility: show title: Formal modelling for Ada implementations: Tasking Event-B ispublished: inpress subjects: ADVANCE subjects: Code_generation subjects: Event-Bsemantics subjects: deploy_tooldev full_text_status: public pres_type: paper abstract: This paper describes a formal modelling approach, where Ada code is automatically generated from the modelling artefacts. We introduce an implementation-level specification, Tasking Event-B, which is an extension to Event-B. Event-B is a formal method, that can be used to model safety-, and business-critical systems. The work may be of interest to a section of the Ada community who are interested in applying formal modelling techniques in their development process, and automatically generating Ada code from the model. We describe a streamlined process, where the abstract modelling artefacts map easily to Ada language constructs. Initial modelling takes place at a high level of abstraction. We then use refinement, decomposition, and finally implementation-level annotations, to generate Ada code. We provide a brief introduction to Event-B, before illustrating the new approach using small examples taken from a larger case study. date: 2012-06 date_type: published event_title: Ada-Europe 2012: 17th International Conference on Reliable Software Technologies event_location: Stockholm event_type: conference refereed: TRUE official_url: http://eprints.soton.ac.uk/335400/ citation: Edmunds, Andrew and Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: Tasking Event-B. In: Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm. (In Press) document_url: http://deploy-eprints.ecs.soton.ac.uk/375/1/AdaEurope2012.pdf