{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T08:29:02Z","timestamp":1726388942573},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319684987"},{"type":"electronic","value":"9783319684994"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68499-4_11","type":"book-chapter","created":{"date-parts":[[2017,10,18]],"date-time":"2017-10-18T10:35:37Z","timestamp":1508322937000},"page":"160-172","source":"Crossref","is-referenced-by-count":4,"title":["B-PERFect"],"prefix":"10.1007","author":[{"given":"Alexandra","family":"Halchin","sequence":"first","affiliation":[]},{"given":"Abderrahmane","family":"Feliachi","sequence":"additional","affiliation":[]},{"given":"Neeraj Kumar","family":"Singh","sequence":"additional","affiliation":[]},{"given":"Yamine","family":"Ait-Ameur","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Ordioni","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,10,19]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM 1999 \u2014 Formal Methods","author":"P Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369\u2013387. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48119-2_22"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-319-33951-1_15","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"N Benaissa","year":"2016","unstructured":"Benaissa, N., Bonvoisin, D., Feliachi, A., Ordioni, J.: The PERF approach for formal verification. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 203\u2013214. Springer, Cham (2016). doi: 10.1007\/978-3-319-33951-1_15"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-45236-2_7","volume-title":"FME 2003: Formal Methods","author":"D Bert","year":"2003","unstructured":"Bert, D., Boulm\u00e9, S., Potet, M.-L., 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\u2013113. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45236-2_7"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-15075-8_1","volume-title":"Formal Methods: Foundations and Applications","author":"R Bonichon","year":"2015","unstructured":"Bonichon, R., D\u00e9harbe, D., Lecomte, T., Medeiros, V.: LLVM-based code generation for B. In: Braga, C., Mart\u00ed-Oliet, N. (eds.) SBMF 2014. LNCS, vol. 8941, pp. 1\u201316. Springer, Cham (2015). doi: 10.1007\/978-3-319-15075-8_1"},{"doi-asserted-by":"crossref","unstructured":"Cata\u00f1o, N., Wahls, T., Rueda, C., Rivera, V., Yu, D.: Translating B machines to JML specifications. In: SAC 2012, pp. 1271\u20131277. ACM (2012)","key":"11_CR6","DOI":"10.1145\/2245276.2231978"},{"unstructured":"ClearSy: Atelier B user manual version 4.0 (2009)","key":"11_CR7"},{"issue":"4","key":"11_CR8","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"unstructured":"Espresso: Polychrony tool. http:\/\/www.irisa.fr\/espresso\/Polychrony","key":"11_CR9"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-319-10181-1_20","volume-title":"Integrated Formal Methods","author":"A F\u00fcrst","year":"2014","unstructured":"F\u00fcrst, A., Hoang, T.S., Basin, D., Desai, K., Sato, N., Miyazaki, K.: Code generation for Event-B. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 323\u2013338. Springer, Cham (2014). doi: 10.1007\/978-3-319-10181-1_20"},{"issue":"9","key":"11_CR11","doi-asserted-by":"crossref","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305\u20131320 (1991)","journal-title":"Proc. IEEE"},{"doi-asserted-by":"crossref","unstructured":"Kalla, H., Talpin, J.P., Berner, D., Besnard, L.: Automated translation of C\/C++ models into a synchronous formalism. In: ECBS 2006. pp. 9\u2013436, March 2006","key":"11_CR12","DOI":"10.1109\/ECBS.2006.27"},{"issue":"4","key":"11_CR13","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/j.infsof.2005.05.002","volume":"48","author":"A Mammar","year":"2006","unstructured":"Mammar, A., Laleau, R.: From a B formal specification to an executable code: application to the relational database domain. Info. Soft. Technol. 48(4), 253\u2013279 (2006)","journal-title":"Info. Soft. Technol."},{"doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.K.: Automatic code generation from EVENT-B models. In: SoICT 2011, pp. 179\u2013188. ACM (2011)","key":"11_CR14","DOI":"10.1145\/2069216.2069252"},{"doi-asserted-by":"crossref","unstructured":"Ge, N., Dieumegard, A., Jenn, E., Voisin, L.: Correct-by-construction specification to verified code. Ada-Europe 2017 (2017)","key":"11_CR15","DOI":"10.1002\/smr.1959"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-19458-5_1","volume-title":"Formal Methods for Industrial Critical Systems","author":"M Petit-Doche","year":"2015","unstructured":"Petit-Doche, M., Breton, N., Courbis, R., Fonteneau, Y., G\u00fcdemann, M.: Formal verification of industrial critical software. In: N\u00fa\u00f1ez, M., G\u00fcdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 1\u201311. Springer, Cham (2015). doi: 10.1007\/978-3-319-19458-5_1"},{"issue":"2","key":"11_CR17","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"MR Prasad","year":"2005","unstructured":"Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. Int. J. Softw. Tools Technol. Transf. 7(2), 156\u2013173 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-58555-9_104","volume-title":"FME 1994: Industrial Benefit of Formal Methods","author":"AC Storey","year":"1994","unstructured":"Storey, A.C., Haughton, H.P.: A strategy for the production of verifiable code using the B Method. In: Naftalin, M., Denvir, T., Bertran, M. (eds.) FME 1994. LNCS, vol. 873, pp. 346\u2013365. Springer, Heidelberg (1994). doi: 10.1007\/3-540-58555-9_104"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-39893-6_18","volume-title":"Formal Methods and Software Engineering","author":"B Tatibou\u00ebt","year":"2003","unstructured":"Tatibou\u00ebt, B., Requet, A., Voisinet, J.-C., Hammad, A.: Java card code generation from B specifications. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 306\u2013318. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-39893-6_18"}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68499-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,4]],"date-time":"2019-10-04T20:45:48Z","timestamp":1570221948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68499-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319684987","9783319684994"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68499-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}