{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:57:20Z","timestamp":1725490640195},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733690"},{"type":"electronic","value":"9783540733706"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73370-6_16","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T20:03:26Z","timestamp":1188417806000},"page":"243-262","source":"Crossref","is-referenced-by-count":13,"title":["Model Extraction for ARINC 653 Based Avionics Software"],"prefix":"10.1007","author":[{"given":"Pedro","family":"de la C\u00e1mara","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mar\u00eda","family":"del Mar Gallardo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pedro","family":"Merino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"ARINC. ARINC Specification 653-2: Avionics Application Software Standard Interface Part 1 - Required Services. Aeronautical Radio INC, Maryland, USA (2005)"},{"key":"16_CR2","unstructured":"ARINC. ARINC Specification 653-2: Avionics Application Software Standard Interface Part 3 - Conformity Test Specification. Aeronautical Radio INC, Maryland, USA (2006)"},{"key":"16_CR3","first-page":"423","volume-title":"Proc. of the FIP TC6 WG6.1 Joint Int. Conf. FORTE XI \/ PSTV XVIII \u201998","author":"D. Bosnacki","year":"1998","unstructured":"Bosnacki, D., Dams, D.: Integrating Real Time into SPIN: A Prototype Implementation. In: Proc. of the FIP TC6 WG6.1 Joint Int. Conf. FORTE XI \/ PSTV XVIII \u201998, pp. 423\u2013438. Kluwer, B.V, Boston, MA (1998)"},{"key":"16_CR4","first-page":"439","volume-title":"ICSE 2000","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S.: Bandera: Extracting finite-state models from java source code. In: ICSE 2000. Proc.of the 22nd Int. Conf. on Software Engineering, pp. 439\u2013448. ACM Press, New York (2000)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11691617_11","volume-title":"Model Checking Software","author":"P. C\u00e1mara de la","year":"2006","unstructured":"de la C\u00e1mara, P., Gallardo, M.M., Merino, P.: Abstract matching for software model checking. In: Valmari, A. (ed.) Model Checking Software. LNCS, vol.\u00a03925, pp. 182\u2013200. Springer, Heidelberg (2006)"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/1081180.1081184","volume-title":"FMICS 2005","author":"P. C\u00e1mara de la","year":"2005","unstructured":"de la C\u00e1mara, P., Gallardo, M.M., Merino, P., San\u00e1n, D.: Model checking software with well-defined apis: the socket case. In: FMICS 2005. Proc. of the 10th Int. Workshop on Formal methods for Industrial Critical Systems, pp. 17\u201326. ACM Press, New York (2005)"},{"issue":"4","key":"16_CR7","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model Checking Java Programs using Java Pathfinder. International Journal of Software Tools for Technology Transfer\u00a02(4), 366\u2013381 (2000)","journal-title":"International Journal of Software Tools for Technology Transfer"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Joshi, R.: Model-driven Software Verification. In: 11th Int. Workshop on Model Checking of Software (SPIN04), pp. 76\u201391 (2004)","DOI":"10.1007\/978-3-540-24732-6_6"},{"issue":"2","key":"16_CR9","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1002\/stvr.228","volume":"11","author":"G.J. Holzmann","year":"2001","unstructured":"Holzmann, G.J., Smith, M.H.: Software model checking: Extracting Verification Models from Source Code. Software Testing, Verification & Reliability\u00a011(2), 65\u201379 (2001)","journal-title":"Software Testing, Verification & Reliability"},{"key":"16_CR10","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1145\/337180.337364","volume-title":"ICSE 2000","author":"W. John Penix","year":"2000","unstructured":"John Penix, W., Visser, E., Engstrom, A.: Verification of Time Partitioning in the DEOS Scheduler Kernel. In: ICSE 2000. Proceedings of the 22nd Int. Conf. on Software Engineering, pp. 488\u2013497. ACM Press, New York (2000)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/3-540-61042-1_53","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Tripakis","year":"1996","unstructured":"Tripakis, S., Courcoubetis, C.: Extending Promela and Spin for Real Time. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 329\u2013348. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73370-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,23]],"date-time":"2019-02-23T03:42:02Z","timestamp":1550893322000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73370-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540733690","9783540733706"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73370-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}