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. © 2012 Springer-Verlag.
CITATION STYLE
Edmunds, A., Rezazadeh, A., & Butler, M. (2012). Formal modelling for Ada implementations: Tasking Event-B. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7308 LNCS, pp. 119–132). https://doi.org/10.1007/978-3-642-30598-6_9
Mendeley helps you to discover research relevant for your work.