{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T05:09:49Z","timestamp":1769749789004,"version":"3.49.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,1,15]],"date-time":"2013-01-15T00:00:00Z","timestamp":1358208000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1007\/s10703-012-0182-0","type":"journal-article","created":{"date-parts":[[2013,1,14]],"date-time":"2013-01-14T10:15:05Z","timestamp":1358158505000},"page":"29-60","source":"Crossref","is-referenced-by-count":21,"title":["Time-triggered runtime verification"],"prefix":"10.1007","volume":"43","author":[{"given":"Borzoo","family":"Bonakdarpour","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samaneh","family":"Navabpour","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Fischmeister","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,1,15]]},"reference":[{"key":"182_CR1","unstructured":"SNU real-time benchmarks. http:\/\/www.cprover.org\/goto-cc\/examples\/snu.html"},{"issue":"2","key":"182_CR2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill D (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"182_CR3","first-page":"87","volume-title":"Proceedings of the 10th international conference on advances in theory and practice of abstract state machines","author":"C Artho","year":"2003","unstructured":"Artho C, Drusinksy D, Goldberg A, Havelund K, Lowry M, Pasareanu C, Ro\u015fu G, Visser W (2003) Experiments with test case generation and runtime analysis. In: Proceedings of the 10th international conference on advances in theory and practice of abstract state machines, ASM\u201903, pp 87\u2013108"},{"key":"182_CR4","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1007\/978-3-540-24622-0_5","volume-title":"Proceedings of the 5th international conference on verification, model checking, and abstract interpretation","author":"H Barringer","year":"2004","unstructured":"Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification. In: Proceedings of the 5th international conference on verification, model checking, and abstract interpretation, VMCAI\u201904, pp 44\u201357"},{"key":"182_CR5","unstructured":"Bauer A, Leucker M, Schallhart C Runtime verification for LTL and TLTL. ACM transactions on software Engineering and Methodology (TOSEM) (2009, in press)"},{"issue":"3","key":"182_CR6","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A Bauer","year":"2010","unstructured":"Bauer A, Leucker M, Schallhart C (2010) Comparing LTL semantics for runtime verification. J Log Comput 20(3):651\u2013674","journal-title":"J Log Comput"},{"issue":"4","key":"182_CR7","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):14","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"182_CR8","first-page":"5","volume-title":"International conference on software engineering (ICSE)","author":"E Bodden","year":"2010","unstructured":"Bodden E (2010) Efficient hybrid typestate analysis by determining continuation-equivalent states. In: International conference on software engineering (ICSE), pp 5\u201314"},{"key":"182_CR9","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/978-3-540-77395-5_3","volume-title":"Proceedings of the 7th international conference on runtime verification","author":"E Bodden","year":"2007","unstructured":"Bodden E, Hendren L, Lam P, Lhot\u00e1k O, Naeem N (2007) Collaborative runtime verification with tracematches. In: Proceedings of the 7th international conference on runtime verification, RV\u201907, pp 22\u201337"},{"key":"182_CR10","first-page":"525","volume-title":"Proceedings of the 21st European conference on object-oriented programming","author":"E Bodden","year":"2007","unstructured":"Bodden E, Hendren L, Lhot\u00e1k O (2007) A staged static program analysis to improve the performance of runtime monitoring. In: Proceedings of the 21st European conference on object-oriented programming, ECOOP\u201907, pp 525\u2013549"},{"key":"182_CR11","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/1453101.1453109","volume-title":"Proceedings of the 16th ACM SIGSOFT international symposium on foundations of software engineering","author":"E Bodden","year":"2008","unstructured":"Bodden E, Lam P, Hendren L (2008) Finding programming errors earlier by evaluating runtime monitors ahead-of-time. In: Proceedings of the 16th ACM SIGSOFT international symposium on foundations of software engineering, FSE\u201908, pp 36\u201347"},{"key":"182_CR12","first-page":"88","volume-title":"Formal methods (FM)","author":"B Bonakdarpour","year":"2011","unstructured":"Bonakdarpour B, Navabpour S, Fischmeister S (2011) Sampling-based runtime verification. In: Formal methods (FM), pp 88\u2013102"},{"key":"182_CR13","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1007\/3-540-55719-9_97","volume-title":"Automata, languages and programming (ICALP)","author":"EY Chang","year":"1992","unstructured":"Chang EY, Manna Z, Pnueli A (1992) Characterization of temporal property classes. In: Automata, languages and programming (ICALP), pp 474\u2013486"},{"key":"182_CR14","first-page":"546","volume-title":"Tools and algorithms for the construction and analysis of systems (TACAS)","author":"F Chen","year":"2005","unstructured":"Chen F, Ro\u015fu G (2005) Java-MOP: a monitoring oriented programming environment for Java. In: Tools and algorithms for the construction and analysis of systems (TACAS), pp 546\u2013550"},{"key":"182_CR15","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1007\/978-3-540-31980-1_36","volume-title":"Proceedings of the 11th international conference on tools and algorithms for the construction and analysis of systems","author":"F Chen","year":"2005","unstructured":"Chen F, Ro\u015fu G (2005) Java-mop: a monitoring oriented programming environment for Java. In: Proceedings of the 11th international conference on tools and algorithms for the construction and analysis of systems, TACAS\u201905, pp 546\u2013550"},{"key":"182_CR16","series-title":"LNCS","volume-title":"Run-time verification","author":"S Colin","year":"2005","unstructured":"Colin S, Mariani L (2005) Run-time verification. LNCS, vol 3472. Springer, Berlin. Chapter 18"},{"key":"182_CR17","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/11513988_36","volume-title":"Computer aided verification (CAV)","author":"M d\u2019Amorim","year":"2005","unstructured":"d\u2019Amorim M, Rosu G (2005) Efficient monitoring of omega-languages. In: Computer aided verification (CAV), pp 364\u2013378"},{"key":"182_CR18","first-page":"220","volume-title":"Proceedings of the 29th international conference on software engineering","author":"MB Dwyer","year":"2007","unstructured":"Dwyer MB, Kinneer A, Elbaum S (2007) Adaptive online program analysis. In: Proceedings of the 29th international conference on software engineering, ICSE \u201907, pp 220\u2013229"},{"key":"182_CR19","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/978-3-642-04694-0_4","volume-title":"Runtime verification (RV)","author":"Y Falcone","year":"2009","unstructured":"Falcone Y, Fernandez J-C, Mounier L (2009) Runtime verification of safety-progress properties. In: Runtime verification (RV), pp 40\u201359"},{"key":"182_CR20","first-page":"133","volume-title":"ACM international conference on languages, compilers, and tools for embedded systems (LCTES)","author":"S Fischmeister","year":"2010","unstructured":"Fischmeister S, Ba Y (2010) Sampling-based program execution monitoring. In: ACM international conference on languages, compilers, and tools for embedded systems (LCTES), pp 133\u2013142"},{"key":"182_CR21","first-page":"412","volume-title":"Automated software engineering (ASE)","author":"D Giannakopoulou","year":"2001","unstructured":"Giannakopoulou D, Havelund K (2001) Automata-based verification of temporal properties on running programs. In: Automated software engineering (ASE), pp 412\u2013416"},{"key":"182_CR22","volume-title":"Proceedings of the 20th IFIP TC 6\/WG 6.1 international conference on testing of software and communicating systems: 8th international workshop","author":"K Havelund","year":"2008","unstructured":"Havelund K (2008) Runtime verification of C programs. In: Proceedings of the 20th IFIP TC 6\/WG 6.1 international conference on testing of software and communicating systems: 8th international workshop, TestCom \u201908\/FATES \u201908"},{"key":"182_CR23","first-page":"374","volume-title":"Verify your runs","author":"K Havelund","year":"2008","unstructured":"Havelund K, Goldberg A (2008) Verify your runs, pp 374\u2013383"},{"issue":"2","key":"182_CR24","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1016\/S1571-0661(04)00253-1","volume":"55","author":"K Havelund","year":"2001","unstructured":"Havelund K, Rosu G (2001) Monitoring Java programs with Java PathExplorer. Electron Notes Theor Comput Sci 55(2):200\u2013217","journal-title":"Electron Notes Theor Comput Sci"},{"key":"182_CR25","first-page":"135","volume-title":"Automated software engineering (ASE)","author":"K Havelund","year":"2001","unstructured":"Havelund K, Rosu G (2001) Monitoring programs using rewriting. In: Automated software engineering (ASE), pp 135\u2013143"},{"key":"182_CR26","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and algorithms for the construction and analysis of systems (TACAS)","author":"K Havelund","year":"2002","unstructured":"Havelund K, Rosu G (2002) Synthesizing monitors for safety properties. In: Tools and algorithms for the construction and analysis of systems (TACAS), pp 342\u2013356"},{"issue":"2","key":"182_CR27","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K Havelund","year":"2004","unstructured":"Havelund K, Rosu G (2004) Efficient monitoring of safety properties. Softw Tools Technol Transf 6(2):158\u2013173","journal-title":"Softw Tools Technol Transf"},{"issue":"3","key":"182_CR28","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/s10009-010-0184-4","volume":"14","author":"X Huang","year":"2012","unstructured":"Huang X, Seyster J, Callanan S, Dixit K, Grosu R, Smolka SA, Stoller SD, Zadok E (2012) Software monitoring with controllable overhead. Softw Tools Technol Transf 14(3):327\u2013347","journal-title":"Softw Tools Technol Transf"},{"key":"182_CR29","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-1-4684-2001-2_9","volume-title":"Symposium on complexity of computer computations","author":"RM Karp","year":"1972","unstructured":"Karp RM (1972) Reducibility among combinatorial problems. In: Symposium on complexity of computer computations, pp 85\u2013103"},{"issue":"4","key":"182_CR30","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/S1571-0661(04)80579-6","volume":"70","author":"M Kim","year":"2002","unstructured":"Kim M, Lee I, Sammapun U, Shin J, Sokolsky O (2002) Monitoring, checking, and steering of real-time systems. Electron Notes Theor Comput Sci 70(4):95\u2013111","journal-title":"Electron Notes Theor Comput Sci"},{"key":"182_CR31","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1109\/EMRTS.1999.777457","volume-title":"Euromicro conference on real-time systems (ECRTS)","author":"M Kim","year":"1999","unstructured":"Kim M, Viswanathan M, Ben-Abdallah H, Kannan S, Lee I, Sokolsky O (1999) Formally specified monitoring of temporal properties. In: Euromicro conference on real-time systems (ECRTS), pp 114\u2013122"},{"issue":"2","key":"182_CR32","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1023\/B:FORM.0000017719.43755.7c","volume":"24","author":"M Kim","year":"2004","unstructured":"Kim M, Viswanathan M, Kannan S, Lee I, Sokolsky O (2004) Java-mac: a run-time assurance approach for Java programs. Form Methods Syst Des 24(2):129\u2013155","journal-title":"Form Methods Syst Des"},{"issue":"2","key":"182_CR33","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1023\/B:FORM.0000017719.43755.7c","volume":"24","author":"M Kim","year":"2004","unstructured":"Kim M, Viswanathan M, Kannan S, Lee I, Sokolsky O (2004) Java-MaC: a run-time assurance approach for Java programs. Form Methods Syst Des 24(2):129\u2013155","journal-title":"Form Methods Syst Des"},{"key":"182_CR34","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer aided verification (CAV)","author":"O Kupferman","year":"1999","unstructured":"Kupferman O, Vardi MY (1999) Model checking of safety properties. In: Computer aided verification (CAV), pp 172\u2013183"},{"key":"182_CR35","first-page":"75","volume-title":"International symposium on code generation and optimization: feedback directed and runtime optimization","author":"C Lattner","year":"2004","unstructured":"Lattner C, Adve V (2004) LLVM: a compilation framework for lifelong program analysis and transformation. In: International symposium on code generation and optimization: feedback directed and runtime optimization, p 75"},{"key":"182_CR36","first-page":"279","volume-title":"Parallel and distributed processing techniques and applications (PDPTA)","author":"I Lee","year":"1999","unstructured":"Lee I, Kannan S, Kim M, Sokolsky O, Viswanathan M (1999) Runtime assurance based on formal specifications. In: Parallel and distributed processing techniques and applications (PDPTA), pp 279\u2013287"},{"key":"182_CR37","unstructured":"ILP solver lp_solve. http:\/\/lpsolve.sourceforge.net\/5.5\/"},{"key":"182_CR38","first-page":"377","volume-title":"Principles of distributed computing (PODC)","author":"Z Manna","year":"1990","unstructured":"Manna Z, Pnueli A (1990) A hierarchy of temporal properties. In: Principles of distributed computing (PODC), pp 377\u2013410"},{"issue":"2","key":"182_CR39","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/s10515-010-0063-y","volume":"17","author":"P Meredith","year":"2010","unstructured":"Meredith P, Jin D, Chen F, Ro\u015fu G (2010) Efficient monitoring of parametric context-free patterns. Autom Softw Eng 17(2):149\u2013180","journal-title":"Autom Softw Eng"},{"key":"182_CR40","first-page":"208","volume-title":"International conference on runtime verification (RV)","author":"S Navabpour","year":"2011","unstructured":"Navabpour S, Wu CW, Bonakdarpour B, Fischmeister S (2011) Efficient techniques for near-optimal instrumentation in time-triggered runtime verification. In: International conference on runtime verification (RV), pp 208\u2013222"},{"key":"182_CR41","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/978-3-642-16612-9_26","volume-title":"Runtime verification (RV)","author":"L Pike","year":"2010","unstructured":"Pike L, Goodloe A, Morisset R, Niller S (2010) Copilot: a hard real-time runtime monitor. In: Runtime verification (RV), pp 345\u2013359"},{"key":"182_CR42","first-page":"46","volume-title":"Symposium on foundations of computer science (FOCS)","author":"A Pnueli","year":"1977","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Symposium on foundations of computer science (FOCS), pp 46\u201357"},{"key":"182_CR43","first-page":"573","volume-title":"Symposium on formal methods (FM)","author":"A Pnueli","year":"2006","unstructured":"Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: Symposium on formal methods (FM), pp 573\u2013586"},{"issue":"3","key":"182_CR44","first-page":"247","volume":"4","author":"J-F Raskin","year":"1999","unstructured":"Raskin J-F, Schobbens P-Y (1999) The logic of event clocks\u2014decidability, complexity and expressiveness. J Autom Lang Comb 4(3):247\u2013286","journal-title":"J Autom Lang Comb"},{"key":"182_CR45","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/978-3-540-89247-2_4","volume-title":"Runtime verification (RV)","author":"G Rosu","year":"2008","unstructured":"Rosu G, Chen F, Ball T (2008) Synthesizing monitors for safety properties: this time with calls and returns. In: Runtime verification (RV), pp 51\u201368"},{"key":"182_CR46","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/978-3-642-16612-9_31","volume-title":"Runtime verification (RV)","author":"J Seyster","year":"2010","unstructured":"Seyster J, Dixit K, Huang X, Grosu R, Havelund K, Smolka SA, Stoller SD, Zadok E (2010) Aspect-oriented instrumentation with GCC. In: Runtime verification (RV), pp 405\u2013420"},{"key":"182_CR47","first-page":"193","volume-title":"Runtime verification (RV)","author":"SD Stoller","year":"2011","unstructured":"Stoller SD, Bartocci E, Seyster J, Grosu R, Havelund K, Smolka SA, Zadok E (2011) Runtime verification with state estimation. In: Runtime verification (RV), pp 193\u2013207"},{"issue":"4","key":"182_CR48","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/j.entcs.2006.02.007","volume":"144","author":"V Stolz","year":"2006","unstructured":"Stolz V, Bodden E (2006) Temporal assertions using AspectJ. Electron Notes Theor Comput Sci 144(4):109\u2013124","journal-title":"Electron Notes Theor Comput Sci"},{"key":"182_CR49","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-642-04694-0_13","volume-title":"Runtime verification (RV)","author":"W Zhou","year":"2009","unstructured":"Zhou W, Sokolsky O, Loo BT, Lee I (2009) MaC: distributed monitoring and checking. In: Runtime verification (RV), pp 184\u2013201"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0182-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0182-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0182-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,8]],"date-time":"2019-07-08T04:11:58Z","timestamp":1562559118000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0182-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,15]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["182"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0182-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,1,15]]}}}