{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T17:06:52Z","timestamp":1748365612133,"version":"3.37.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319929965"},{"type":"electronic","value":"9783319929972"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-92997-2_17","type":"book-chapter","created":{"date-parts":[[2018,5,28]],"date-time":"2018-05-28T08:13:16Z","timestamp":1527495196000},"page":"264-278","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model-Driven Re-engineering of a Pressure Sensing System: An Experience Report"],"prefix":"10.1007","author":[{"given":"Atif","family":"Mashkoor","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felix","family":"Kossak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mikl\u00f3s","family":"Bir\u00f3","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Egyed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,29]]},"reference":[{"key":"17_CR1","unstructured":"Atelier B Translators: User Manual version 4.6. http:\/\/tools.clearsy.com\/resources\/documents . Accessed 28 Feb 2018"},{"key":"17_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B Book. Cambridge University Press, Cambridge (1996)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Formal methods in industry: achievements, problems, future. In: Proceedings of the 28th International Conference on Software Engineering ICSE 2006, pp. 761\u2013768. ACM, New York (2006)","DOI":"10.1145\/1134285.1134406"},{"key":"17_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Formal validation and verification of a medical software critical component. In: 13. ACM\/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015, pp. 80\u201389. Austin, 21\u201323 September 2015","DOI":"10.1109\/MEMCOD.2015.7340473"},{"key":"17_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2011.11.014","volume":"208","author":"M Benveniste","year":"2011","unstructured":"Benveniste, M.: On using B in the design of secure micro-controllers: an experience report. Electron. Notes Theor. Comput. Sci. 208, 3\u201322 (2011)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"17_CR7","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). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_7"},{"key":"17_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines: A Method for High-Level System Design and Analysis","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., Stark, R.F.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag New York Inc., Secaucus (2003)"},{"issue":"4","key":"17_CR9","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28(4), 626\u2013643 (1996)","journal-title":"ACM Comput. Surv."},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-24431-5_7","volume-title":"Formal Methods for Industrial Critical Systems","author":"I Daskaya","year":"2011","unstructured":"Daskaya, I., Huhn, M., Milius, S.: Formal safety analysis in industrial practice. In: Sala\u00fcn, G., Sch\u00e4tz, B. (eds.) FMICS 2011. LNCS, vol. 6959, pp. 68\u201384. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24431-5_7"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-30885-7_33","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"A Edmunds","year":"2012","unstructured":"Edmunds, A., Butler, M., Maamria, I., Silva, R., Lovell, C.: Event-B code generation: type extension with theories. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 365\u2013368. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30885-7_33"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Fitzgerald, J.S., Larsen, P.G.: Triumphs and challenges for model-oriented formal methods: the VDM++ experience. In: Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2006), pp. 1\u20134, November 2006","DOI":"10.1109\/ISoLA.2006.33"},{"key":"17_CR13","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). https:\/\/doi.org\/10.1007\/978-3-319-10181-1_20"},{"key":"17_CR14","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)"},{"key":"17_CR15","volume-title":"Systematic Software Development Using VDM","author":"CB Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall Inc., Upper Saddle River (1990)","edition":"2"},{"key":"17_CR16","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-319-07512-9_10","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"F Kossak","year":"2014","unstructured":"Kossak, F.: Landing gear system: an ASM-based solution for the ABZ case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 142\u2013147. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_10"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-33600-8_13","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"F Kossak","year":"2016","unstructured":"Kossak, F., Mashkoor, A.: How to select the suitable formal method for an industrial application: a survey. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 213\u2013228. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_13"},{"key":"17_CR18","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)"},{"key":"17_CR19","unstructured":"Lecomte, T.: Atelier B has turned twenty. In: Keynote of the Fifth International Conference on ASMs, Alloy, B, TLA, VDM, and Z (ABZ 2016). Springer, Heidelberg (2016)"},{"issue":"2","key":"17_CR20","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. J. Softw. Tools Technol. Transf. 10(2), 185\u2013203 (2008)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-319-33600-8_29","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A Mashkoor","year":"2016","unstructured":"Mashkoor, A.: The hemodialysis machine case study. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 329\u2013343. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_29"},{"issue":"3","key":"17_CR22","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/s11219-015-9288-0","volume":"24","author":"A Mashkoor","year":"2016","unstructured":"Mashkoor, A.: Model-driven development of high-assurance active medical devices. Softw. Q. J. 24(3), 571\u2013596 (2016). https:\/\/doi.org\/10.1007\/s11219-015-9288-0","journal-title":"Softw. Q. J."},{"issue":"1","key":"17_CR23","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/LES.2015.2494459","volume":"8","author":"A Mashkoor","year":"2016","unstructured":"Mashkoor, A., Biro, M.: Towards the trustworthy development of active medical devices: a hemodialysis case study. IEEE Embed. Syst. Lett. 8(1), 14\u201317 (2016)","journal-title":"IEEE Embed. Syst. Lett."},{"key":"17_CR24","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-319-13251-8_8","volume-title":"Software Quality. Software and Systems Quality in Distributed and Mobile Environments","author":"A Mashkoor","year":"2015","unstructured":"Mashkoor, A., Biro, M., Dolgos, M., Timar, P.: Refinement-based development of software-controlled safety-critical active medical devices. In: Winkler, D., Biffl, S., Bergsmann, J. (eds.) SWQD 2015. LNBIP, vol. 200, pp. 120\u2013132. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-13251-8_8"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-642-40588-4_21","volume-title":"Security Engineering and Intelligence Informatics","author":"A Mashkoor","year":"2013","unstructured":"Mashkoor, A., Hasan, O., Beer, W.: Using probabilistic analysis for the certification of machine control systems. In: Cuzzocrea, A., Kittl, C., Simos, D.E., Weippl, E., Xu, L. (eds.) CD-ARES 2013. LNCS, vol. 8128, pp. 305\u2013320. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40588-4_21"},{"key":"17_CR26","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 2011, pp. 179\u2013188. ACM, New York (2011)","DOI":"10.1145\/2069216.2069252"},{"issue":"2","key":"17_CR27","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/1646353.1646372","volume":"53","author":"SP Miller","year":"2010","unstructured":"Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58\u201364 (2010)","journal-title":"Commun. ACM"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-10431-7_14","volume-title":"Software Engineering and Formal Methods","author":"R Reicherdt","year":"2014","unstructured":"Reicherdt, R., Glesner, S.: Formal verification of discrete-time MATLAB\/Simulink models using boogie. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 190\u2013204. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_14"},{"key":"17_CR29","volume-title":"Understanding Z: A Specification Language and Its Formal Semantics","author":"JM Spivey","year":"1988","unstructured":"Spivey, J.M.: Understanding Z: A Specification Language and Its Formal Semantics. Cambridge University Press, Cambridge (1988)"},{"key":"17_CR30","unstructured":"Wright, S.: Automatic generation of C from Event-B. In: Workshop on Integration of Model-based Formal Methods and Tools (2009)"}],"container-title":["Lecture Notes in Computer Science","Modelling Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-92997-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T13:58:08Z","timestamp":1571407088000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-92997-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319929965","9783319929972"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-92997-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}