{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:04:56Z","timestamp":1725573896561},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_21","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T10:35:57Z","timestamp":1294396557000},"page":"359-374","source":"Crossref","is-referenced-by-count":0,"title":["Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures"],"prefix":"10.1007","author":[{"given":"Micka\u00ebl","family":"Kerb\u0153uf","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Nowak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45828-X_19","volume-title":"Embedded Software","author":"A. Benveniste","year":"2002","unstructured":"Benveniste, A., Caspi, P., Guernic, P.L., Marchand, H., Talpin, J.-P., Tripakis, S.: A protocol for loosely time-triggered architectures. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol.\u00a02491. Springer, Heidelberg (2002)"},{"issue":"2","key":"21_CR2","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0167-6423(91)90001-E","volume":"16","author":"A. Benveniste","year":"1991","unstructured":"Benveniste, A., Le Guernic, P.: Synchronous Programming with Events and Relations: the Signal Language and its Semantics. Science of Computer Programming\u00a016(2), 103\u2013149 (1991)","journal-title":"Science of Computer Programming"},{"key":"21_CR3","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The Esterel Synchronous Programming Language: Design, Semantics, Implementation. Science of Computer Programming\u00a019, 87\u2013152 (1992)","journal-title":"Science of Computer Programming"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-48249-0_34","volume-title":"Computer Safety, Reliability and Security","author":"P. Caspi","year":"1999","unstructured":"Caspi, P., Mazuet, C., Salem, R., Weber, D.: Formal design of distributed control systems with lustre. In: Felici, M., Kanoun, K., Pasquini, A. (eds.) SAFECOMP 1999. LNCS, vol.\u00a01698, p. 396. Springer, Heidelberg (1999)"},{"issue":"9","key":"21_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. Proc. of the IEEE\u00a079(9), 1305\u20131320 (1991)","journal-title":"Proc. of the IEEE"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-44659-1_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Kerboeuf","year":"2000","unstructured":"Kerboeuf, M., Nowak, D., Talpin, J.-P.: Specification and verification of a steamboiler with Signal-Coq. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 356\u2013371. Springer, Heidelberg (2000)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/3-540-44618-4_41","volume-title":"CONCUR 2000 - Concurrency Theory","author":"R. Lazi\u0107","year":"2000","unstructured":"Lazi\u0107, R., Nowak, D.: A unifying approach to data-independence. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 581\u2013595. Springer, Heidelberg (2000)"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/BFb0055148","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Nowak","year":"1998","unstructured":"Nowak, D., Beauvais, J.-R., Talpin, J.-P.: Co-inductive axiomatization of a synchronous language. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 387\u2013399. Springer, Heidelberg (1998)"},{"key":"21_CR9","unstructured":"The Coq development team. The Coq proof assistant reference manual: Version 7.3.1. Technical report, INRIA (2002)"},{"key":"21_CR10","unstructured":"Werner, B.: Une Th\u00e9orie des Constructions Inductives. PhD thesis, Universit\u00e9 Paris VII (1994)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39893-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T05:37:35Z","timestamp":1553319455000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}