{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:54:11Z","timestamp":1740099251550,"version":"3.37.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030047702"},{"type":"electronic","value":"9783030047719"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-04771-9_16","type":"book-chapter","created":{"date-parts":[[2018,12,5]],"date-time":"2018-12-05T17:02:53Z","timestamp":1544029373000},"page":"205-215","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Exploring Applications of Formal Methods in the INSPEX Project"],"prefix":"10.1007","author":[{"given":"Joseph","family":"Razavi","sequence":"first","affiliation":[]},{"given":"Richard","family":"Banach","sequence":"additional","affiliation":[]},{"given":"Olivier","family":"Debicki","sequence":"additional","affiliation":[]},{"given":"Nicolas","family":"Mareau","sequence":"additional","affiliation":[]},{"given":"Suzanne","family":"Lesecq","sequence":"additional","affiliation":[]},{"given":"Julie","family":"Foucault","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,12,6]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Formal methods in industry: achievements, problems future. In: Proceedings ACM\/IEEE ICSE 2006, pp. 761\u2013768 (2006)","DOI":"10.1145\/1134285.1134406"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. CUP (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"16_CR3","unstructured":"Banach, R. (ed.): Special issue on the state of the art in formal methods. J. Univ. Comput. Sci. 13(5) (2007)"},{"key":"16_CR4","unstructured":"Barnes, J.E.: Experiences in the industrial use of formal methods. Electron. Commun. EASST 46 (2011)"},{"key":"16_CR5","unstructured":"Bawa: \nhttps:\/\/www.bawa.tech\/"},{"key":"16_CR6","unstructured":"BLAST Tool (2011). \nhttps:\/\/forge.ispras.ru\/projects\/blast\/"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/52.391826","volume":"12","author":"J Bowen","year":"1995","unstructured":"Bowen, J., Hinchey, M.: Seven more Myths of formal methods. IEEE Softw. 12, 34\u201341 (1995)","journal-title":"IEEE Softw."},{"key":"16_CR8","volume-title":"Software Engineering: Modern Approaches","author":"E Braude","year":"2011","unstructured":"Braude, E., Bernstein, M.: Software Engineering: Modern Approaches. Wiley, Hoboken (2011)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-30885-7_14","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D D\u00e9harbe","year":"2012","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for Rodin. In: Derrick, J., et al. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194\u2013207. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-30885-7_14"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-319-25423-4_11","volume-title":"Formal Methods and Software Engineering","author":"S Divakaran","year":"2015","unstructured":"Divakaran, S., D\u2019Souza, D., Kushwah, A., Sampath, P., Sridhar, N., Woodcock, J.: Refinement-based verification of the FreeRTOS Scheduler in VCC. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 170\u2013186. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-25423-4_11"},{"key":"16_CR11","unstructured":"Facebook: \nhttps:\/\/en-gb.facebook.com"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-642-33826-7_6","volume-title":"Software Engineering and Formal Methods","author":"A Salehi Fathabadi","year":"2012","unstructured":"Salehi Fathabadi, A., Butler, M., Rezazadeh, A.: A Systematic approach to atomicity decomposition in Event-B. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 78\u201393. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-33826-7_6"},{"key":"16_CR13","unstructured":"FreeRTOS: (2017). \nhttps:\/\/www.freertos.org\/"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/52.57887","volume":"7","author":"A Hall","year":"1990","unstructured":"Hall, A.: Seven Myths of formal methods. IEEE Softw. 7, 11\u201319 (1990)","journal-title":"IEEE Softw."},{"key":"16_CR15","volume-title":"Mathematical Techniques in Multisensor Data Fusion","author":"D Hall","year":"2004","unstructured":"Hall, D.: Mathematical Techniques in Multisensor Data Fusion. Artech House, Norwood (2004)"},{"key":"16_CR16","first-page":"1395","volume":"55","author":"J Harrison","year":"2008","unstructured":"Harrison, J.: Formal proof\u2014theory and practice. Not. AMS 55, 1395\u20131406 (2008)","journal-title":"Not. AMS"},{"key":"16_CR17","unstructured":"IEC 62304: \nhttps:\/\/webstore.iec.ch\/publication\/22794"},{"key":"16_CR18","unstructured":"INSPEX Homepage: (2017). \nhttp:\/\/www.inspex-ssi.eu\/"},{"key":"16_CR19","doi-asserted-by":"publisher","DOI":"10.1142\/10282","volume-title":"Statistical Data Fusion","author":"B Kedem","year":"2017","unstructured":"Kedem, B., De Oliveira, V., Sverchkov, M.: Statistical Data Fusion. World Scientific, Singapore (2017)"},{"key":"16_CR20","unstructured":"Meyer, B.: How you will be programming ten years from now. In: ACM SAC-10 Keynote (2010)"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Moravec, H., Elfes, A.: High resolution maps from wide angle sonar. In: Proceedings IEEE ICRA (1985)","DOI":"10.1109\/ROBOT.1985.1087316"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-59293-8_189","volume-title":"TAPSOFT \u201995: Theory and Practice of Software Development","author":"V Pratt","year":"1995","unstructured":"Pratt, V.: Anatomy of the Pentium bug. In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds.) CAAP 1995. LNCS, vol. 915, pp. 97\u2013107. Springer, Heidelberg (1995). \nhttps:\/\/doi.org\/10.1007\/3-540-59293-8_189"},{"key":"16_CR23","volume-title":"Software Engineering: A Practitioner\u2019s Approach","author":"R Pressman","year":"2005","unstructured":"Pressman, R.: Software Engineering: A Practitioner\u2019s Approach. McGraw Hill, New York City (2005)"},{"key":"16_CR24","unstructured":"ProB Tool: \nhttps:\/\/www3.hhu.de\/stups\/prob\/"},{"key":"16_CR25","unstructured":"Rango: (2018). \nhttp:\/\/www.gosense.com\/rango\/"},{"key":"16_CR26","unstructured":"RODIN Tool: (2018). \nhttp:\/\/sourceforge.net\/projects\/rodin-b-sharp\/\n\n\nhttp:\/\/www.event-b.org\/"},{"key":"16_CR27","doi-asserted-by":"publisher","first-page":"3047","DOI":"10.1109\/TIM.2012.2202169","volume":"61","author":"L Scalise","year":"2012","unstructured":"Scalise, L., Primiani, V., Russo, P.: Experimental investigation of electromagnetic obstacle detection for visually impaired users: a comparison with ultrasonic sensing. IEEE Trans. Inst. Meas. 61, 3047\u20133057 (2012)","journal-title":"IEEE Trans. Inst. Meas."},{"key":"16_CR28","unstructured":"Smartcane: (2017). \nhttps:\/\/www.phoenixmedicalsystems.com\/assistive-technology\/smartcane\/"},{"key":"16_CR29","volume-title":"Software Engineering","author":"I Sommerville","year":"2015","unstructured":"Sommerville, I.: Software Engineering. Pearson, London (2015)"},{"key":"16_CR30","volume-title":"Probabilistic Robotics","author":"S Thrun","year":"2005","unstructured":"Thrun, S., Burgard, W., Fox, D.: Probabilistic Robotics. MIT Press, Cambridge (2005)"},{"key":"16_CR31","unstructured":"Ultracane: (2017). \nhttps:\/\/www.ultracane.com\/"},{"key":"16_CR32","unstructured":"Verhoef, M.: From documents to models: towards digital continuity. In: SAFECOMP\/IMBSA-17 Keynote. \nhttps:\/\/drive.google.com\/file\/d\/0B9DzO9PFER2xZDRxLUpKVUdYZmM\/view?usp=sharing"}],"container-title":["Lecture Notes in Computer Science","Software Technologies: Applications and Foundations"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-04771-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,12,5]],"date-time":"2018-12-05T17:11:54Z","timestamp":1544029914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-04771-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030047702","9783030047719"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-04771-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"STAF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Federation of International Conferences on Software Technologies: Applications and Foundations","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toulouse","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 June 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 June 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"staf2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.staf2018.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}