{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:36:10Z","timestamp":1725543370716},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540372158"},{"type":"electronic","value":"9783540372165"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11813040_12","type":"book-chapter","created":{"date-parts":[[2006,8,7]],"date-time":"2006-08-07T10:51:03Z","timestamp":1154947863000},"page":"163-178","source":"Crossref","is-referenced-by-count":10,"title":["Towards Modularized Verification of Distributed Time-Triggered Systems"],"prefix":"10.1007","author":[{"given":"Jewgenij","family":"Botaschanjan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Gruler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Harhurin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonid","family":"Kof","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maria","family":"Spichkova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Trachtenherz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"The MathWorks (May 18, 2006), http:\/\/www.mathworks.com"},{"key":"12_CR2","unstructured":"IBM Rational Rose Technical Developer (May 18, 2006), http:\/\/www-306.ibm.com\/software\/awdtools\/developer\/technical\/"},{"key":"12_CR3","unstructured":"AutoFocus (May 18, 2006), http:\/\/autofocus.in.tum.de\/"},{"key":"12_CR4","unstructured":"FlexRay Consortium: FlexRay Communication System - Protocol Specification - Version 2.0 (2004)"},{"key":"12_CR5","unstructured":"OSEK\/VDX: Time-Triggered Operating System - Specification 1.0 (May 18, 2006)"},{"key":"12_CR6","unstructured":"European Commission (DG Enterprise and DG Information Society): eSafety forum: Summary report 2003. Technical report, eSafety (2003)"},{"issue":"1","key":"12_CR7","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/2.248873","volume":"27","author":"H. Kopetz","year":"1994","unstructured":"Kopetz, H., Gr\u00fcnsteidl, G.: TTP \u2014 a protocol for fault-tolerant real-time systems. Computer\u00a027(1), 14\u201323 (1994)","journal-title":"Computer"},{"key":"12_CR8","unstructured":"VxWorks: A Realtime Operating System (RTOS) (May 18, 2006), http:\/\/www.windriver.com"},{"key":"12_CR9","unstructured":"QNX: A Realtime Operating System (RTOS) (May 18, 2006), http:\/\/www.qnx.com"},{"key":"12_CR10","unstructured":"OSEK\/VDX (May18, 2006), http:\/\/www.osek-vdx.org"},{"key":"12_CR11","unstructured":"TTP\/C (May 18, 2006), http:\/\/www.vmars.tuwien.ac.at\/projects\/ttp\/ttpc.html"},{"key":"12_CR12","unstructured":"TTCan: Time Triggered Communication on CAN (May 18, 2006), http:\/\/www.ttcan.com"},{"key":"12_CR13","unstructured":"FlexRay Consortium (May 18, 2006), http:\/\/www.flexray.com"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Botaschanjan, J., Kof, L., K\u00fchnel, C., Spichkova, M.: Towards Verified Automotive Software. In: ICSE, SEAS Workshop, St. Louis, Missouri, USA (2005)","DOI":"10.1145\/1083190.1083199"},{"key":"12_CR15","unstructured":"OSEK\/VDX: Fault-Tolerant Communication - Specification 1.0 (May 18, 2006), http:\/\/portal.osek-vdx.org\/files\/pdf\/specs\/ftcom10.pdf"},{"key":"12_CR16","unstructured":"FlexRay Consortium: FlexRay Communication System - Bus Guardian Specification - Version 2.0 (2004)"},{"key":"12_CR17","unstructured":"FlexRay Consortium: FlexRay Communication System - Electrical Physical Layer Specification - Version 2.0 (2004)"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/3-540-63533-5_7","volume-title":"FME \u201997 Industrial Applications and Strengthened Foundations of Formal Methods","author":"F. Huber","year":"1997","unstructured":"Huber, F., Sch\u00e4tz, B., Einert, G.: Consistent Graphical Specification of Distributed Systems. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol.\u00a01313, pp. 122\u2013141. Springer, Heidelberg (1997)"},{"key":"12_CR19","unstructured":"Verisoft Project (May 18, 2006), http:\/\/www.verisoft.de"},{"key":"12_CR20","unstructured":"Verisoft\u2013Automotive Project (May 18, 2006), http:\/\/www4.in.tum.de\/~verisoft\/automotive"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Leinenbach, D., Paul, W., Petrova, E.: Towards the Formal Verification of a C0 Compiler. In: 3rd International Conference on SEFM, Koblenz, Germany, pp. 2\u201312 (2005)","DOI":"10.1109\/SEFM.2005.51"},{"key":"12_CR22","unstructured":"The Motor Industry Software Reliability Association (MISRA): Guidelines for the Use of the C Language in Critical Systems. Motor Industry Research Association (MIRA), Ltd., UK (May 18, 2006)"},{"key":"12_CR23","unstructured":"AbsInt Angewandte Informatik GmbH. Worst-Case Execution Time Analyzers (May 18, 2006), http:\/\/www.absint.com\/profile.htm"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"12_CR25","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.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An open source tool for symbolic model checking. In: Proceedings of CAV 2002, Copenhagen, Denmark (2002) 359\u2013364"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Wimmel, G., L\u00f6tzbeyer, H., Pretschner, A., Slotosch, O.: Specification based test sequence generation with propositional logic. Journal of STVR: Special Issue on Specification Based Testing, 229\u2013248 (2000)","DOI":"10.1002\/1099-1689(200012)10:4<229::AID-STVR213>3.0.CO;2-O"},{"issue":"1","key":"12_CR27","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/JPROC.2002.805820","volume":"91","author":"J. Sifakis","year":"2003","unstructured":"Sifakis, J., Tripakis, S., Yovine, S.: Building models of real-time systems from application software. Proceedings of the IEEE\u00a091(1), 100\u2013111 (2003)","journal-title":"Proceedings of the IEEE"},{"key":"12_CR28","first-page":"203","volume-title":"Dependable Computing for Critical Applications\u20146","author":"J. Rushby","year":"1997","unstructured":"Rushby, J.: Systematic formal verification for fault-tolerant time-triggered algorithms. In: Dependable Computing for Critical Applications\u20146, vol.\u00a011, pp. 203\u2013222. IEEE Computer Society, Los Alamitos (1997)"},{"key":"12_CR29","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/JPROC.2002.805825","volume":"91","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Horowitz, B., Kirsch, C.M.: Giotto: A time-triggered language for embedded programming. Proceedings of the IEEE\u00a091, 84\u201399 (2003)","journal-title":"Proceedings of the IEEE"},{"key":"12_CR30","unstructured":"Bauer, A., Romberg, J.: Model-Based Deployment in Automotive Embedded Software: From a High-Level View to Low-Level Implementations. In: Proceedings of MOMPES, satelite of ACSD 2004, Hamilton, Canada, pp. 93\u2013106 (2004)"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kirsch, C.M., Majumdar, R., Matic, S.: Time-safety checking for embedded programs. In: EMSOFT 2002, pp. 76\u201392 (2002)","DOI":"10.1007\/3-540-45828-X_7"},{"key":"12_CR32","first-page":"211","volume-title":"The automotive CASE","author":"P. Braun","year":"2003","unstructured":"Braun, P., Broy, M., Cengarle, M.V., Philipps, J., Prenninger, W., Pretschner, A., Rappl, M., Sandner, R.: The automotive CASE, pp. 211\u2013228. Wiley, Chichester (2003)"},{"key":"12_CR33","unstructured":"ASCET-SD (May 18, 2006), http:\/\/de.etasgroup.com\/products\/ascet"},{"key":"12_CR34","unstructured":"Cadence Cierto VCC (May 18, 2006), http:\/\/www.cadence.com"}],"container-title":["Lecture Notes in Computer Science","FM 2006: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11813040_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:14:18Z","timestamp":1605644058000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11813040_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372158","9783540372165"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/11813040_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}