{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T03:01:38Z","timestamp":1725678098756},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642299513"},{"type":"electronic","value":"9783642299520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29952-0_14","type":"book-chapter","created":{"date-parts":[[2012,5,3]],"date-time":"2012-05-03T06:14:09Z","timestamp":1336025649000},"page":"84-93","source":"Crossref","is-referenced-by-count":1,"title":["Automatic Verification of Real-Time Systems with Rich Data: An Overview"],"prefix":"10.1007","author":[{"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"14_CR1","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10270-006-0009-9","volume":"6","author":"F. Arbab","year":"2007","unstructured":"Arbab, F., Baier, C., de Boer, F.S., Rutten, J.J.M.M.: Models and temporal logical specifications for timed component connectors. Soft. and Syst. Modeling\u00a06(1), 59\u201382 (2007)","journal-title":"Soft. and Syst. Modeling"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/3-540-60472-3_4","volume-title":"Hybrid Systems II","author":"A. Bouajjani","year":"1995","unstructured":"Bouajjani, A., Echahed, R., Robbana, R.: On the Automatic Verification of Systems with Continuous Variables and Unbounded Discrete Data Structures. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol.\u00a0999, pp. 64\u201385. Springer, Heidelberg (1995)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s Decidable About Arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2005)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-73210-5_4","volume-title":"Integrated Formal Methods","author":"I. Br\u00fcckner","year":"2007","unstructured":"Br\u00fcckner, I.: Slicing Concurrent Real-Time System Specifications for Verification. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 54\u201374. Springer, Heidelberg (2007)"},{"key":"14_CR5","unstructured":"Br\u00fcckner, I.: Slicing Integrated Formal Specifications for Verification. PhD thesis, Report Nr. 2\/08, University of Oldenburg (March 2008)"},{"issue":"4","key":"14_CR6","first-page":"369","volume":"89","author":"I. Br\u00fcckner","year":"2008","unstructured":"Br\u00fcckner, I., Dr\u00e4ger, K., Finkbeiner, B., Wehrheim, H.: Slicing abstractions. Fundamenta Informaticae\u00a089(4), 369\u2013392 (2008)","journal-title":"Fundamenta Informaticae"},{"issue":"4","key":"14_CR7","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/1805950.1805953","volume":"11","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log.\u00a011(4), Article 23, 38 (2010)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1-3","key":"14_CR8","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(02)00743-0","volume":"302","author":"Z. Dang","year":"2003","unstructured":"Dang, Z.: Pushdown timed automata: a binary reachability characterization and safety verification. Theor. Comput. Sci.\u00a0302(1-3), 93\u2013121 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"14_CR9","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1109\/TSE.2008.52","volume":"34","author":"J.S. Dong","year":"2008","unstructured":"Dong, J.S., Hao, P., Qin, S., Sun, J., Yi, W.: Timed automata patterns. IEEE Trans. Software Eng.\u00a034(6), 844\u2013859 (2008)","journal-title":"IEEE Trans. Software Eng."},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-540-85361-9_17","volume-title":"CONCUR 2008 - Concurrency Theory","author":"K. Dr\u00e4ger","year":"2008","unstructured":"Dr\u00e4ger, K., Finkbeiner, B.: Subsequence Invariants. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol.\u00a05201, pp. 172\u2013186. Springer, Heidelberg (2008)"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-642-12002-2_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Dr\u00e4ger","year":"2010","unstructured":"Dr\u00e4ger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 271\u2013274. Springer, Heidelberg (2010)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-16265-7_11","volume-title":"Integrated Formal Methods","author":"J. Faber","year":"2010","unstructured":"Faber, J.: Verification Architectures: Compositional Reasoning for Real-Time Systems. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol.\u00a06396, pp. 136\u2013151. Springer, Heidelberg (2010)"},{"key":"14_CR13","unstructured":"Faber, J.: Verification Architecture for Complex Real-Time Systems. PhD thesis, Report Nr. 03\/11, University of Oldenburg (August 2011)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-16265-7_12","volume-title":"Integrated Formal Methods","author":"J. Faber","year":"2010","unstructured":"Faber, J., Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: Automatic Verification of Parametric Specifications with Complex Topologies. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol.\u00a06396, pp. 152\u2013167. Springer, Heidelberg (2010)"},{"issue":"1-2","key":"14_CR15","first-page":"117","volume":"5","author":"J. Faber","year":"2011","unstructured":"Faber, J., Linker, S., Olderog, E.-R., Quesel, J.-D.: Syspect - modelling, specifying, and verifying real-time systems with rich data. International Journal of Software and Informatics\u00a05(1-2), 117\u2013137 (2011)","journal-title":"International Journal of Software and Informatics"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-71209-1_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Hansen, M.R.: Deciding an Interval Logic with Accumulated Durations. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 201\u2013215. Springer, Heidelberg (2007)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Giese, H., Tichy, M., Burmester, S., Sch\u00e4fer, W., Flake, S.: Towards the compositional verification of real-time UML designs. In: ESEC\/FSE-11, pp. 38\u201347. ACM (2003)","DOI":"10.1145\/949952.940078"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modeling and analysis of an audio\/video protocol: an industrial case study using UPPAAL. In: IEEE Real-Time Systems Symposium (RTSS), pp. 1\u201313. IEEE Computer Society (1997)","DOI":"10.7146\/brics.v4i31.18957"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-03237-0_7","volume-title":"Static Analysis","author":"M. Heizmann","year":"2009","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of Trace Abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 69\u201385. Springer, Heidelberg (2009)"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Hermenegildo, M.V., Palsberg, J. (eds.) Principles of Programming Languages (POPL), pp. 471\u2013482. Association for Computing Machinery. ACM (2010)","DOI":"10.1145\/1707801.1706353"},{"key":"14_CR21","unstructured":"Hoenicke, J.: Combination of Processes, Data, and Time. PhD thesis, Report Nr. 9\/2006, University of Oldenburg (July 2006)"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-642-15375-4_32","volume-title":"CONCUR 2010 - Concurrency Theory","author":"J. Hoenicke","year":"2010","unstructured":"Hoenicke, J., Meyer, R., Olderog, E.-R.: Kleene, Rabin, and Scott Are Available. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 462\u2013477. Springer, Heidelberg (2010)"},{"issue":"4","key":"14_CR23","first-page":"301","volume":"9","author":"J. Hoenicke","year":"2002","unstructured":"Hoenicke, J., Olderog, E.-R.: CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic J. of Comput.\u00a09(4), 301\u2013334 (2002)","journal-title":"Nordic J. of Comput."},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On Local Reasoning in Verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 265\u2013281. Springer, Heidelberg (2008)"},{"key":"14_CR25","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-02959-2_9","volume-title":"Automated Deduction \u2013 CADE-22","author":"C. Ihlemann","year":"2009","unstructured":"Ihlemann, C., Sofronie-Stokkermans, V.: System Description: H-PILoT. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol.\u00a05663, pp. 131\u2013139. Springer, Heidelberg (2009)"},{"key":"14_CR26","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-14203-1_4","volume-title":"Automated Reasoning","author":"C. Ihlemann","year":"2010","unstructured":"Ihlemann, C., Sofronie-Stokkermans, V.: On Hierarchical Reasoning in Combinations of Theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol.\u00a06173, pp. 30\u201345. Springer, Heidelberg (2010)"},{"key":"14_CR27","unstructured":"Janssen, W.: Layered Design of Parallel Systems. PhD thesis, Univ. Twente (1994)"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-540-75221-9_18","volume-title":"Formal Methods and Hybrid Real-Time Systems","author":"J. Knudsen","year":"2007","unstructured":"Knudsen, J., Ravn, A.P., Skou, A.: Design Verification Patterns. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol.\u00a04700, pp. 399\u2013413. Springer, Heidelberg (2007)"},{"key":"14_CR29","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s00236-010-0121-8","volume":"47","author":"R. Lanotte","year":"2010","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Reachability results for timed automata with unbounded data structures. Acta Informatica\u00a047, 279\u2013311 (2010)","journal-title":"Acta Informatica"},{"key":"14_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"Computer Aided Verification","author":"S. McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.C.: Data Structure Specifications via Local Equality Axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 476\u2013490. Springer, Heidelberg (2005)"},{"issue":"4-5","key":"14_CR31","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s00165-008-0082-7","volume":"20","author":"R. Meyer","year":"2008","unstructured":"Meyer, R., Faber, J., Hoenicke, J., Rybalchenko, A.: Model checking duration calculus: A practical approach. Formal Aspects of Comput.\u00a020(4-5), 481\u2013505 (2008)","journal-title":"Formal Aspects of Comput."},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"Olderog, E.-R.: Automatic verification of combined specifications. In: Pu, G., Stolz, V. (eds.) Proc. of the 1st Internat. Workshop on Harnessing Theories for Tool Support in Software, Macau. ENTCS, vol.\u00a0207, pp. 3\u201316 (2008)","DOI":"10.1016\/j.entcs.2008.03.082"},{"key":"14_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-15297-9_18","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"E.-R. Olderog","year":"2010","unstructured":"Olderog, E.-R., Swaminathan, M.: Layered Composition for Timed Automata. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol.\u00a06246, pp. 228\u2013242. Springer, Heidelberg (2010)"},{"key":"14_CR34","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1016\/j.tcs.2008.09.022","volume":"410","author":"P.C. \u00d6lveczky","year":"2009","unstructured":"\u00d6lveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude. Theor. Comput. Sci.\u00a0410, 254\u2013280 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2006","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2006)"},{"key":"14_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-00255-7_7","volume-title":"Integrated Formal Methods","author":"J. St\u00f6cker","year":"2009","unstructured":"St\u00f6cker, J., Lang, F., Garavel, H.: Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol.\u00a05423, pp. 88\u2013102. Springer, Heidelberg (2009)"},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"Taibi, T. (ed.): Design patterns formalization techniques. IGI Publishing (2007)","DOI":"10.4018\/978-1-59904-219-0"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Models of Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29952-0_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:22:42Z","timestamp":1620127362000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29952-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642299513","9783642299520"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29952-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}