{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T09:43:54Z","timestamp":1773308634929,"version":"3.50.1"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2015,5,6]],"date-time":"2015-05-06T00:00:00Z","timestamp":1430870400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,2]]},"DOI":"10.1007\/s10009-015-0381-2","type":"journal-article","created":{"date-parts":[[2015,5,5]],"date-time":"2015-05-05T11:54:20Z","timestamp":1430826860000},"page":"31-52","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":39,"title":["Code generation for Event-B"],"prefix":"10.1007","volume":"19","author":[{"given":"V\u00edctor","family":"Rivera","sequence":"first","affiliation":[]},{"given":"N\u00e9stor","family":"Cata\u00f1o","sequence":"additional","affiliation":[]},{"given":"Tim","family":"Wahls","sequence":"additional","affiliation":[]},{"given":"Camilo","family":"Rueda","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,5,6]]},"reference":[{"key":"381_CR1","unstructured":"Abrial, J.-R.: Sequential program development: teaching resources (2009). http:\/\/deploy-eprints.ecs.soton.ac.uk\/122\/1\/sld.ch15%2Cseq.pdf . Accessed March 2015"},{"key":"381_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Design","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Design. Cambridge University Press, New York (2010)"},{"issue":"6","key":"381_CR3","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Son Hoang, T., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Softw. Tools Technol. Transf."},{"issue":"1,2","key":"381_CR4","first-page":"1","volume":"77","author":"J-R Abrial","year":"2007","unstructured":"Abrial, J.-R., Hallerstede, S.: Refinement, decomposition and instantiation of discrete models: application to Event-B. Fundamentae Informatica 77(1,2), 1\u201324 (2007)","journal-title":"Fundamentae Informatica"},{"key":"381_CR5","first-page":"343","volume-title":"On the Construction of Programs","author":"J-R Abrial","year":"1980","unstructured":"Abrial, J.-R., Schuman, S., Meyer, B.: Specification language. In: McKeag, R., Macnaghten, A. (eds.) On the Construction of Programs, pp. 343\u2013410. Cambridge University Press, Cambridge, UK (1980)"},{"key":"381_CR6","first-page":"17","volume":"12","author":"R Back","year":"1991","unstructured":"Back, R., Sere, K.: Stepwise refinement of action systems. Struct. Progr. 12, 17\u201330 (1991)","journal-title":"Struct. Progr."},{"key":"381_CR7","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"J Barnes","year":"2003","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley Longman Publishing Co., Inc., Boston (2003)"},{"issue":"6","key":"381_CR8","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1049\/sej.1991.0040","volume":"6","author":"G Bernot","year":"1991","unstructured":"Bernot, G., Gaudel, M., Marre, B.: Software testing based on formal specifications: a theory and a tool. Softw. Eng. J. 6(6), 387\u2013405 (1991)","journal-title":"Softw. Eng. J."},{"key":"381_CR9","volume-title":"Managing the Testing Process","author":"R Black","year":"2009","unstructured":"Black, R.: Managing the Testing Process. Wiley Publishing Inc, Hoboken, NJ (2009)"},{"key":"381_CR10","doi-asserted-by":"crossref","unstructured":"Bouquet, F., Couchot, J., Dadeau, F., Giorgetti, A.: Instantiation of Parameterized Data Structures for Model-Based Testing. In: B\u20192007, the 7th International B Conference, vol. 4355 of LNCS, pp. 96\u2013110. Springer (2007)","DOI":"10.1007\/11955757_10"},{"key":"381_CR11","doi-asserted-by":"crossref","unstructured":"Bouquet, F., Dadeau, F., Groslambert, J.: Checking JML specifications with B machines. In: Proceedings of Formal Specification and Development in Z and B, vol. 3455 of Lecture Notes in Computer Science, pp. 435\u2013454, Guildford, U.K. Springer (2005)","DOI":"10.1007\/11415787_25"},{"key":"381_CR12","doi-asserted-by":"crossref","unstructured":"Bouquet, F., Dadeau, F., Groslambert, J.: JML2B: Checking JML specifications with B machines. In: Proceedings of B: Formal Specification and Development in B, vol. 4355 of Lecture Notes in Computer Science, pp. 285\u2013288. Springer, Berlin\/Heidelberg, Besanc\u0303on, France (2006)","DOI":"10.1007\/11955757_31"},{"issue":"3","key":"381_CR13","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G., Leino, K., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212\u2013232 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"381_CR14","doi-asserted-by":"crossref","unstructured":"Butler, M.: Decomposition Structures for Event-B. In: Proceedings of the 7th International Conference on Integrated Formal Methods, IFM \u201909, pp. 20\u201338, Berlin, Heidelberg. Springer (2009)","DOI":"10.1007\/978-3-642-00255-7_2"},{"key":"381_CR15","doi-asserted-by":"crossref","unstructured":"Cata\u00f1o, N., Rueda, C., Wahls, T.: A machine-checked proof for a translation of Event-B machines to JML. ArXiv e-prints (2013)","DOI":"10.1002\/9781119002727.ch9"},{"key":"381_CR16","doi-asserted-by":"crossref","unstructured":"Cata\u00f1o, N., Huisman, M.: Chase: a static checker for JML\u2019s assignable clause. In: Zuck, L., Attie, P., Cortesi, A., Mukhopadhyay, S. (eds.) Verification, Model Checking, and Abstract Interpretation, vol. 2575 of Lecture Notes in Computer Science, pp. 26\u201340, New York, NY, USA. Springer (2003)","DOI":"10.1007\/3-540-36384-X_6"},{"key":"381_CR17","doi-asserted-by":"crossref","unstructured":"Cata\u00f1o, N., Rueda, C.: Teaching formal methods for the unconquered territory. In: 2nd International Formal Methods Europe Conference on Teaching Formal Methods, Lecture Notes in Computer Science, The Netherlands. Springer (2009)","DOI":"10.1007\/978-3-642-04912-5_2"},{"key":"381_CR18","doi-asserted-by":"crossref","unstructured":"Cata\u00f1o, N., Rueda, C.: Matelas: A Predicate Calculus Common Formal Definition for Social Networking. In: Frappier, M. (ed.) Proceedings of ABZ 2010, vol. 5977 of Lecture Notes in Computer Science, pp. 259\u2013272, Qu\u00e9bec, Canada. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-11811-1_20"},{"key":"381_CR19","doi-asserted-by":"crossref","unstructured":"Cata\u00f1o, N., Wahls, T., Rueda, C., Rivera, V., Yu, D.: Translating B machines to JML specifications. In: 27th ACM Symposium on Applied Computing, Software Verification and Testing track (SAC-SVT), Trento, Italy. ACM (2012)","DOI":"10.1145\/2245276.2231978"},{"key":"381_CR20","volume-title":"Portuguese forum of Informatics (INFORUM)","author":"N Cata\u00f1o","year":"2010","unstructured":"Cata\u00f1o, N., Pestana, J., Rodrigues, R.: JFly: a JML-based strategy for incorporating formal specifications into the software development process. In: Barbosa, L., Correia, M.P. (eds.) Portuguese forum of Informatics (INFORUM). Braga, Portugal (2010)"},{"issue":"5","key":"381_CR21","doi-asserted-by":"crossref","first-page":"614","DOI":"10.1007\/s11241-013-9182-4","volume":"49","author":"A Cavalcanti","year":"2013","unstructured":"Cavalcanti, A., Zeyda, F., Wellings, A., Woodcock, J., Wei, K.: Safety-critical Java programs from Circus models. Real-Time Syst. 49(5), 614\u2013667 (2013)","journal-title":"Real-Time Syst."},{"key":"381_CR22","doi-asserted-by":"crossref","unstructured":"Cok, D.: OpenJML: JML for Java 7 by Extending OpenJDK. In: NASA Formal Methods Symposium, pp. 472\u2013479 (2011)","DOI":"10.1007\/978-3-642-20398-5_35"},{"key":"381_CR23","unstructured":"Damchoom, K.: An incremental refinement approach to a development of a flash-based file system in Event-B. Ph.D. thesis, University of Southampton (2010)"},{"key":"381_CR24","unstructured":"Edmunds, A., Butler, M.: Tool support for Event-B code generation. In: Workshop on Tool Building in Formal Methods, Qu\u00e9bec, Canada. Wiley and Sons (2010)"},{"key":"381_CR25","unstructured":"Edmunds, A., Butler, M.: Tasking Event-B: an extension to Event-B for generating concurrent code. In: PLACES (2011)"},{"key":"381_CR26","unstructured":"Edmunds, A., Rezazedah, A.: Development of a heating controller system (2011). http:\/\/wiki.event-b.org\/index.php\/Development_of_a_Heating_Controller_System . Accessed March 2015"},{"key":"381_CR27","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermann, H. (eds.) Conference on Computer-Aided Verification, vol. 4590 of Lecture Notes in Computer Science, pp. 173\u2013177 (2007)","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"381_CR28","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison Wesley Longman Publishing Co., Inc., Boston (1995)"},{"key":"381_CR29","doi-asserted-by":"crossref","unstructured":"Jin, D., Yang, Z.: Strategies of modeling from VDM-SL to JML. In: International Conference on Advanced Language Processing and Web Information Technology, pp. 320\u2013323, Liaoning, China. IEEE Computer Society (2008)","DOI":"10.1109\/ALPIT.2008.25"},{"key":"381_CR30","unstructured":"Jones, C.: Systematic Software Development Using VDM. International Series in Computer Science, 2nd edn. Prentice Hall (1990)"},{"key":"381_CR31","unstructured":"The KeY Project, Integrated Deductive Software Design. http:\/\/www.key-project.org\/ . Accessed March 2015"},{"issue":"8","key":"381_CR32","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"issue":"3","key":"381_CR33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT 31(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT"},{"key":"381_CR34","doi-asserted-by":"crossref","unstructured":"Leuchel, M., Butler, M.: ProB: a model checker for B. In: Formal Methods Europe: Formal Methods, Lecture Notes in Computer Science, Pisa, Italy. Springer (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"381_CR35","unstructured":"Link, J.: Unit Testing in Java. M. Kaufmann (2003)"},{"key":"381_CR36","unstructured":"Locke, D., Andersen, B., Brosgoal, B., Fulton, M., Henties, T., Hunt, J., Nielsen, J., Schoeberl, M., Tokar, J., Vitek, J., Weillings, A.: Safety Critical Java Specification, version 0.78. Technical report, The Open Group (2010). http:\/\/jcp.org\/aboutJava\/communityprocess\/edr\/jsr302\/index.html . Accessed March 2015"},{"key":"381_CR37","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.K.: Automatic code generation from Event-B models. In: Proceedings of the Second Symposium on Information and Communication Technology, SoICT. ACM (2011)","DOI":"10.1145\/2069216.2069252"},{"issue":"10","key":"381_CR38","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cDesign by Contract\u201d. Computer 25(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"381_CR39","unstructured":"De Moura, L., Bjorner, N.: Z3: an efficient solver (2010). http:\/\/research.microsoft.com\/en-us\/um\/redmond\/projects\/z3\/ . Accessed March 2015"},{"key":"381_CR40","volume-title":"Usability Engineering","author":"J Nielsen","year":"1993","unstructured":"Nielsen, J.: Usability Engineering. AP Professional, San Diego (1993)"},{"key":"381_CR41","doi-asserted-by":"crossref","unstructured":"Ostroumov, S., Tsiopoulos, L.: VHDL code generation from formal Event-B models. In: Proceedings of the 14th Euromicro Conference on Digital System Design, Euromicro Conference on Digital System Design, pp. 127\u2013134. IEEE Computer Society, Washington, DC (2011)","DOI":"10.1109\/DSD.2011.20"},{"key":"381_CR42","unstructured":"Padidar, S.: A study in the use of Event-B for system development from a software engineering viewpoint. Master\u2019s thesis, University of Edinburgh (2010)"},{"key":"381_CR43","unstructured":"Rivera, V., Cata\u00f1o, N.: The Social-Event Planner (2012). http:\/\/poporo.uma.pt\/favas\/Social-Event_Planner.html . Accessed March 2015"},{"key":"381_CR44","doi-asserted-by":"crossref","unstructured":"Rivera, V., Cata\u00f1o, N.: Translating Event-B to JML-specified Java programs. In: ACM Symposium on Applied Computing, Software Verification and Testing track (SAC-SVT), South Korea (2014)","DOI":"10.1145\/2554850.2554897"},{"key":"381_CR45","unstructured":"Sarshogh, M., Butler, M.: Specification and refinement of discrete timing properties in Event-B. Electron Commun. Eur. Assoc. Softw. Sci. Technol. 46 (2011)"},{"key":"381_CR46","unstructured":"Sarshogh, M., Butler, M.: Extending Event-B with discrete timing properties (2012). http:\/\/deploy-eprints.ecs.soton.ac.uk\/401\/1\/Journal.pdf . Accessed March 2015"},{"key":"381_CR47","unstructured":"State-Machines and Code Generation (2012). http:\/\/wiki.event-b.org\/index.php\/State-Machines_and_Code_Generation . Accessed Aug 2013"},{"key":"381_CR48","unstructured":"Toom, A., Naks, T., Pantel, M., Gandriau, M., Indrawati: Gene-Auto: an Automatic code generator for a safe subset of Simulink\/Stateflow and Scicos. In: Akadeemia, I.B., Krates, O.\u00dc., University of Toulouse IRIT-ENSEEIHT, F. Alyotech CRIL Technologies, Tallinn University of Technology (eds.) Embedded Real Time Software (2008)"},{"key":"381_CR49","volume-title":"Concurrent and Real-Time Programming in Java","author":"A Wellings","year":"2004","unstructured":"Wellings, A.: Concurrent and Real-Time Programming in Java. Wiley & Sons, Hoboken, NJ (2004)"},{"key":"381_CR50","unstructured":"Woodcock, J., Davies, J.: Using Z: specification, refinement, and proof. In: International Series in Computer Science. Prentice-Hall Inc. (1996)"},{"key":"381_CR51","unstructured":"Wright, S.: Automatic Generation of C from Event-B. In: Workshop on Integration of Model-based Formal Methods and Tools, Nantes, France. Springer (2009)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0381-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0381-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0381-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0381-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,7]],"date-time":"2022-05-07T05:24:13Z","timestamp":1651901053000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0381-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,6]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,2]]}},"alternative-id":["381"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0381-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,6]]}}}