{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T23:48:10Z","timestamp":1743032890011,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030042080"},{"type":"electronic","value":"9783030042097"}],"license":[{"start":{"date-parts":[[2018,11,20]],"date-time":"2018-11-20T00:00:00Z","timestamp":1542672000000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-04209-7_1","type":"book-chapter","created":{"date-parts":[[2018,11,19]],"date-time":"2018-11-19T16:37:15Z","timestamp":1542645435000},"page":"3-15","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Methods in Systems Integration: Deployment of Formal Techniques in INSPEX"],"prefix":"10.1007","author":[{"given":"Richard","family":"Banach","sequence":"first","affiliation":[]},{"given":"Joe","family":"Razavi","sequence":"additional","affiliation":[]},{"given":"Suzanne","family":"Lesecq","sequence":"additional","affiliation":[]},{"given":"Olivier","family":"Debicki","sequence":"additional","affiliation":[]},{"given":"Nicolas","family":"Mareau","sequence":"additional","affiliation":[]},{"given":"Julie","family":"Foucault","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Correvon","sequence":"additional","affiliation":[]},{"given":"Gabriela","family":"Dudnik","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,11,20]]},"reference":[{"key":"1_CR1","unstructured":"Alloy. http:\/\/alloy.mit.edu\/"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Formal Methods in Industry: Achievements. Problems Future. In: Proceedings of ACM\/IEEE ICSE 2006, pp. 761\u2013768 (2006)","DOI":"10.1145\/1134285.1134406"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. CUP (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Andronick, J., Jeffery, R., Klein, G., Kolanski, R., Staples, M., Zhang, H., Zhu, L.: Large-scale formal verification in practice: a process perspective. In: Proceedings of ACM\/IEEE ICSE 2012, pp. 374\u2013393 (2012)","DOI":"10.1109\/ICSE.2012.6227120"},{"key":"1_CR6","unstructured":"Astr\u00e9e Tool. http:\/\/www.astree.ens.fr\/"},{"key":"1_CR7","unstructured":"Baeten, J.: Process Algebra. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1990)"},{"key":"1_CR8","unstructured":"Banach, R. (ed.): Special Issue on the State of the Art in Formal Methods. Journal of Universal Computer Science, vol. 13(5) (2007)"},{"key":"1_CR9","unstructured":"BLAST Tool. https:\/\/forge.ispras.ru\/projects\/blast\/"},{"key":"1_CR10","unstructured":"Bluetooth Guide. http:\/\/ww1.microchip.com\/downloads\/en\/DeviceDoc\/50002466B.pdf"},{"key":"1_CR11","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 Software 12, 34\u201341 (1995)","journal-title":"IEEE Software"},{"key":"1_CR12","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E Clarke","year":"1996","unstructured":"Clarke, E., Wing, J.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28, 626\u2013643 (1996)","journal-title":"ACM Comput. Surv."},{"issue":"1","key":"1_CR13","doi-asserted-by":"publisher","first-page":"13841","DOI":"10.1016\/j.ifacol.2017.08.2225","volume":"50","author":"Roxana Dia","year":"2017","unstructured":"Dia, R., Mottin, J., Rakotavao, T., Puschini, D., Lesecq, S.: Evaluation of occupancy grid resolution through a novel approach for inverse sensor modeling. In: Proceedings of IFAC World Congress, FAC-PapersOnLine, vol. 50, pp. 13,841\u201313,847 (2017)","journal-title":"IFAC-PapersOnLine"},{"key":"1_CR14","doi-asserted-by":"crossref","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.) Proceedings of ICFEM 2015. LNCS, vol. 9407, pp. 170\u2013186. Springer (2015)","DOI":"10.1007\/978-3-319-25423-4_11"},{"key":"1_CR15","unstructured":"Fausten, M.: Evolution or revolution: architecture of AD cars. In: Proceedings of IEEE ESWEEK (2015)"},{"key":"1_CR16","unstructured":"FDR Tool. https:\/\/www.cs.ox.ac.uk\/projects\/fdr\/"},{"key":"1_CR17","unstructured":"Fitzgerald, J., Gorm\u00a0Larsen, P.: Modelling Systems: Practical Tools and Techniques for Software Development. Cambridge University Press (1998)"},{"key":"1_CR18","unstructured":"FreeRTOS. https:\/\/www.freertos.org\/"},{"key":"1_CR19","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 Software 7, 11\u201319 (1990)","journal-title":"IEEE Software"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Hoare, C.: Communicating Sequential Processes. Prentice-Hall (1985)","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"1_CR21","unstructured":"ISO\/IEC 13568: Information Technology \u2013 Z Formal Specification Notation \u2013 Syntax, Type System and Semantics: International Standard (2002). http:\/\/www.iso.org\/iso\/en\/ittf\/PubliclyAvailableStandards\/c021573_ISO_IEC_13568_2002(E).zip"},{"key":"1_CR22","unstructured":"Jones, C.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall (1990)"},{"issue":"4","key":"1_CR23","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1109\/MC.2006.145","volume":"39","author":"C Jones","year":"2006","unstructured":"Jones, C., O\u2019Hearne, P., Woodcock, J.: Verified software: a grand challenge. IEEE Comput. 39(4), 93\u201395 (2006)","journal-title":"IEEE Comput."},{"key":"1_CR24","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)"},{"key":"1_CR25","unstructured":"Mandruchi, R., Kurniavan, S.: Mobility-Related Accidents Experienced by People with Visual Impairment. Insight: Research and Practice in Visual Impairment and Blindness (2011)"},{"key":"1_CR26","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall (1989)"},{"key":"1_CR27","unstructured":"NuSMV Tool. http:\/\/nusmv.fbk.eu\/"},{"key":"1_CR28","unstructured":"Qu, Z.: Cooperative Control of Dynamical Systems: Applications to Autonomous Vehicles. Springer (2009)"},{"key":"1_CR29","unstructured":"RODIN Tool. http:\/\/www.event-b.org\/ , http:\/\/sourceforge.net\/projects\/rodin-b-sharp\/"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"de\u00a0Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511663079"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Rosburg, T.: Tactile ground surface indicators in public places. In: Grunwald, M. (ed.) Human Haptic Perception: Basics and Applications. Springer, Birkhauser (2008)","DOI":"10.1007\/978-3-7643-7612-3_41"},{"key":"1_CR32","unstructured":"Spivey, J.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall International (1992)"},{"issue":"1","key":"1_CR33","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1093\/combul\/43.1.24","volume":"43","author":"S. Stepney","year":"2001","unstructured":"Stepney, S.: New Horizons in Formal Methods. The Computer Bulletin, pp. 24\u201326 (2001)","journal-title":"The Computer Bulletin"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Stepney, S., Cooper, D.: Formal Methods for Industrial Products. In: Proceedings of 1st Conference of B and Z Users. LNCS, vol. 1878, pp. 374\u2013393. Springer (2000)","DOI":"10.1007\/3-540-44525-0_22"},{"key":"1_CR35","unstructured":"Thrun, S., Burgard, W., Fox, D.: Probabilistic Robotics. MIT Press (2005)"},{"key":"1_CR36","unstructured":"UPPAAL Tool. http:\/\/www.uppaal.org\/"},{"key":"1_CR37","unstructured":"Wikipedia: List of tools for static code analysis. https:\/\/en.wikipedia.org\/wiki\/List_of_tools_ for_static_code_analysis"},{"issue":"10","key":"1_CR38","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1109\/MC.2006.340","volume":"39","author":"J Woodcock","year":"2006","unstructured":"Woodcock, J.: First steps in the the verified software grand challenge. IEEE Computer 39(10), 57\u201364 (2006)","journal-title":"IEEE Computer"},{"key":"1_CR39","first-page":"661","volume":"13","author":"J Woodcock","year":"2007","unstructured":"Woodcock, J., Banach, R.: The verification grand challenge. JUCS 13, 661\u2013668 (2007)","journal-title":"JUCS"}],"container-title":["Complex Systems Design & Management"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-04209-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,5]],"date-time":"2019-11-05T13:20:08Z","timestamp":1572960008000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-04209-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,20]]},"ISBN":["9783030042080","9783030042097"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-04209-7_1","relation":{},"subject":[],"published":{"date-parts":[[2018,11,20]]},"assertion":[{"value":"20 November 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CSD&M","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Complex Systems Design & Management","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","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":"18 December 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 December 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"csdm2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.2018.csdm-asia.net\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}