{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T18:45:12Z","timestamp":1760121912352},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642156533"},{"type":"electronic","value":"9783642156540"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15654-0_4","type":"book-chapter","created":{"date-parts":[[2010,9,30]],"date-time":"2010-09-30T07:40:26Z","timestamp":1285832426000},"page":"61-72","source":"Crossref","is-referenced-by-count":13,"title":["Using Simulink Design Verifier for Proving Behavioral Properties on a Complex Safety Critical System in the Ground Transportation Domain"],"prefix":"10.1007","author":[{"given":"J. -F.","family":"Etienne","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Fechter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E.","family":"Juppeaux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11925040_8","volume-title":"Leveraging Applications of Formal Methods","author":"P.A. Abdulla","year":"2006","unstructured":"Abdulla, P.A., Deneux, J., St\u00e5lmarck, G., \u00c5gren, H., \u00c5kerlund, O.: Designing safe, reliable systems using scade. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol.\u00a04313, pp. 115\u2013129. Springer, Heidelberg (2006)"},{"key":"4_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book, Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B Book, Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Place, J.: Lustre: a declarative language for programming synchronous systems. In: ACM Symp. on Princ. of Prog. Langs., POPL 1987 (1987)","DOI":"10.1145\/41625.41641"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019 (2001)","DOI":"10.1023\/A:1011276507260"},{"issue":"9","key":"4_CR5","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language lustre. Proceedings of the IEEE\u00a079(9), 1305\u20131320 (1991)","journal-title":"Proceedings of the IEEE"},{"key":"4_CR6","unstructured":"MathWorks. Simulink Design Verifier, http:\/\/www.mathworks.com\/products\/sldesignverifier\/"},{"key":"4_CR7","unstructured":"MathWorks, http:\/\/www.mathworks.com\/products\/stateflow\/"},{"key":"4_CR8","unstructured":"MathWorks, Simulink, http:\/\/www.mathworks.com\/products\/simulink\/"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-49519-3_7","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"1998","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on st\u00e5lmarck\u2019s proof procedure for propositional logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 82\u201399. Springer, Heidelberg (1998)"},{"key":"4_CR11","unstructured":"The Coq\u00a0Development Team. Coq, version 8.2. INRIA (February 2009), http:\/\/coq.inria.fr\/"}],"container-title":["Complex Systems Design & Management"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15654-0_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:11:18Z","timestamp":1606187478000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15654-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642156533","9783642156540"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15654-0_4","relation":{},"subject":[],"published":{"date-parts":[[2010]]}}}