{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T20:58:21Z","timestamp":1725829101258},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242545"},{"type":"electronic","value":"9783319242552"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24255-2_7","type":"book-chapter","created":{"date-parts":[[2015,9,5]],"date-time":"2015-09-05T09:51:13Z","timestamp":1441446673000},"page":"74-89","source":"Crossref","is-referenced-by-count":2,"title":["Safely Using the AUTOSAR End-to-End Protection Library"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Arts","sequence":"first","affiliation":[]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,25]]},"reference":[{"unstructured":"ISO 26262: Road vehicles Functional safety (2011)","key":"7_CR1"},{"unstructured":"AUTOSAR: Software architecture specification \n                      www.autosar.org","key":"7_CR2"},{"unstructured":"AUTOSAR. In: Specification of SW-C End-to-End Communication ProtectionLibrary. AUTOSAR consortium (2008\u20132013)","key":"7_CR3"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-319-10506-2_6","volume-title":"Computer Safety, Reliability, and Security","author":"T Arts","year":"2014","unstructured":"Arts, T., Dorigatti, M., Tonetta, S.: Making implicit safety requirements explicit. In: Bondavalli, A., Di Giandomenico, F. (eds.) SAFECOMP 2014. LNCS, vol. 8666, pp. 81\u201392. Springer, Heidelberg (2014)"},{"doi-asserted-by":"crossref","unstructured":"Armstrong, J.: A history of Erlang. In: HOPL, pp. 1\u201326 (2007)","key":"7_CR5","DOI":"10.1145\/1238844.1238850"},{"doi-asserted-by":"crossref","unstructured":"Arts, T., Hughes, J., Johansson, J., Wiger, U.: Testing telecoms software with Quviq QuickCheck. In: ACM SIGPLAN Workshop on Erlang (2006)","key":"7_CR6","DOI":"10.1145\/1159789.1159792"},{"doi-asserted-by":"crossref","unstructured":"Arts, T., Hughes, J., Norell, U., Svensson, H.: Testing AUTOSAR software with QuickCheck. In: Proceedings of TAIC Part 2015 (2015)","key":"7_CR7","DOI":"10.1109\/ICSTW.2015.7107466"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Heidelberg (2014)"},{"doi-asserted-by":"crossref","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: ASE, pp. 702\u2013705 (2013)","key":"7_CR10","DOI":"10.1109\/ASE.2013.6693137"},{"key":"7_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic, Dordrecht (1993)"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","key":"7_CR12","DOI":"10.1109\/SFCS.1977.32"},{"issue":"3","key":"7_CR13","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/s004500050132","volume":"14","author":"M Broy","year":"1999","unstructured":"Broy, M., Huber, F., Sch\u00e4tz, B.: AutoFocus - Ein Werkzeugprototyp zur Entwicklung eingebetteter Systeme. Inform. Forsch. Entwickl. 14(3), 121\u2013134 (1999)","journal-title":"Inform. Forsch. Entwickl."},{"doi-asserted-by":"crossref","unstructured":"Forest, T., Jochim, M.: On the fault detection capabilities of AUTOSAR\u2019s end-to-end communication protection CRC\u2019s. In: SAE (2011)","key":"7_CR14","DOI":"10.4271\/2011-01-0999"},{"doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Parameter synthesis with IC3. In: FMCAD, pp. 165\u2013168 (2013)","key":"7_CR15","DOI":"10.1109\/FMCAD.2013.6679406"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24255-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T17:55:36Z","timestamp":1559238936000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24255-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242545","9783319242552"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24255-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}