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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Russo, A.: Formal Methods in Industry: The State of Practice of Formal Methods in South America and Far East (2009)
Metayer, C., Clabaut, M.: DIR 41 Case Study. In: [27], p. 357
Taft, T., Tucker, R., Brukardt, R., Ploedereder, E. (eds.): Consolidated Ada reference manual: language and standard libraries. Springer-Verlag New York, Inc., New York (2002)
RODIN Project, http://rodin.cs.ncl.ac.uk
The DEPLOY Project Team: Project Website, http://www.deploy-project.eu/
Edmunds, A., Rezazedah, A.: Event-B Wiki: Development of a Heating Controller System, http://wiki.event-b.org/index.php/Development_of_a_Heating_Controller_System
Butler, M.: Decomposition Structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20–38. Springer, Heidelberg (2009)
Silva, R., Pascal, C., Hoang, T., Butler, M.: Decomposition Tool for Event-B. Software: Practice and Experience (2010)
Edmunds, A., Butler, M.: Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In: PLACES 2011 (2011)
Silva, R.: Towards the Composition of Specifications in Event-B. In: B 2011 (2011)
Edmunds, A., Rezazedah, A.: Event-B Project Archives: Tasking Event-B Tutorial. University of Southampton, http://deploy-eprints.ecs.soton.ac.uk/304/
Burns, A., Dobbing, B., Vardanega, T.: Guide for the use of the Ada Ravenscar Profile in high integrity systems. Ada Lett. XXIV, 1–74 (2004)
The Eclipse Project: Eclipse - an Open Development Platform, http://www.eclipse.org/
AdaCore: GNAT Programming Studio, http://www.adacore.com/home/
The Advance Project Team: The Advance Project, http://www.advance-ict.eu
Sarshogh, M., Butler, M.: Specification and Refinement of Discrete Timing Properties in Event-B. In: AVoCS 2011 (2011)
Abrial, J.: The B Book - Assigning Programs to Meanings. Cambridge University Press (1996)
ClearSy System Engineering: The B Language Reference Manual (Version 4.6 edn.)
Bert, D., Boulmé, S., Potet, M., Requet, A., Voisin, L.: Adaptable Translator of B Specifications to Embedded C Programs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 94–113. Springer, Heidelberg (2003)
Stoddart, B., Cansell, D., Zeyda, F.: Modelling and Proof Analysis of Interrupt Driven Scheduling. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 155–170. Springer, Heidelberg (2006)
CSK Systems Corporation: (The VDM++ Language Manual)
Verhoef, M., Larsen, P.G., Hooman, J.: Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 147–162. Springer, Heidelberg (2006)
Degerlund, F., Grönblom, R., Sere, K.: Code Generation and Scheduling of Event-B Models (2011)
Berry, G.: Synchronous Design and Verification of Critical Embedded Systems Using SCADE and Esterel. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, p. 2. Springer, Heidelberg (2008)
Snook, C., Butler, M.: UML-B: A Plug-in for the Event-B Tool Set. In: [27], p. 344
Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.): ABZ 2008. LNCS, vol. 5238. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Edmunds, A., Rezazadeh, A., Butler, M. (2012). Formal Modelling for Ada Implementations: Tasking Event-B. In: Brorsson, M., Pinho, L.M. (eds) Reliable Software Technologies – Ada-Europe 2012. Ada-Europe 2012. Lecture Notes in Computer Science, vol 7308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30598-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-30598-6_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30597-9
Online ISBN: 978-3-642-30598-6
eBook Packages: Computer ScienceComputer Science (R0)