{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T17:52:08Z","timestamp":1777657928303,"version":"3.51.4"},"reference-count":81,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2013,11,7]],"date-time":"2013-11-07T00:00:00Z","timestamp":1383782400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/2.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,6]]},"DOI":"10.1007\/s10703-013-0199-z","type":"journal-article","created":{"date-parts":[[2013,11,6]],"date-time":"2013-11-06T13:53:56Z","timestamp":1383746036000},"page":"203-239","source":"Crossref","is-referenced-by-count":31,"title":["Runtime verification of embedded real-time systems"],"prefix":"10.1007","volume":"44","author":[{"given":"Thomas","family":"Reinbacher","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"F\u00fcgger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00f6rg","family":"Brauer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,11,7]]},"reference":[{"key":"199_CR1","series-title":"LNCS","first-page":"538","volume-title":"CAV","author":"Y Abarbanel","year":"2000","unstructured":"Abarbanel Y, Beer I, Gluhovsky L, Keidar S, Wolfsthal Y (2000) FoCs: automatic generation of simulation checkers from formal specifications. In: CAV. LNCS, vol 1855. Springer, Berlin, pp 538\u2013542"},{"key":"199_CR2","first-page":"390","volume-title":"LICS","author":"R Alur","year":"1990","unstructured":"Alur R, Henzinger TA (1990) Real-time logics: complexity and expressiveness. In: LICS. IEEE, New York, pp 390\u2013401"},{"key":"199_CR3","first-page":"196","volume-title":"TACAS","author":"R Armoni","year":"2002","unstructured":"Armoni R, Fix L, Flaisher A, Gerth R, Ginsburg B, Kanza T, Landver A, Mador-Haim S, Singerman E, Tiemeyer A, Vardi MY, Zbar Y (2002) The Forspec temporal logic: a new temporal property-specification language. In: TACAS. Springer, Berlin, pp 196\u2013211"},{"key":"199_CR4","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/11940197_11","volume-title":"Formal approaches to software testing and runtime verification","author":"R Armoni","year":"2006","unstructured":"Armoni R, Korchemny D, Tiemeyer A, Vardi M, Zbar Y (2006) Deterministic dynamic monitors for linear-time assertions. In: Formal approaches to software testing and runtime verification. LNCS, vol 4262. Springer, Berlin, pp 163\u2013177"},{"key":"199_CR5","first-page":"196","volume-title":"MICRO","author":"TM Austin","year":"1999","unstructured":"Austin TM (1999) DIVA: a reliable substrate for deep submicron microarchitecture design. In: MICRO. IEEE, New York, pp 196\u2013207"},{"key":"199_CR6","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"199_CR7","first-page":"54","volume-title":"VMCAI","author":"S Bardin","year":"2011","unstructured":"Bardin S, Herrmann P, V\u00e9drine F (2011) Refinement-based CFG reconstruction from unstructured programs. In: VMCAI. Springer, Berlin, pp 54\u201369"},{"key":"199_CR8","series-title":"LNCS","volume-title":"RV","author":"B Barre","year":"2012","unstructured":"Barre B, Klein M, Soucy-Boivin M, Ollivier PA, Hall\u00e9 S (2012) MapReduce for parallel trace validation of LTL properties. In: RV. LNCS. Springer, Berlin"},{"key":"199_CR9","series-title":"LNCS","volume-title":"Runtime verification\u2014first international conference, proceedings","year":"2010","unstructured":"Barringer H, Falcone Y, Finkbeiner B, Havelund K, Lee I, Pace GJ, Rosu G, Sokolsky O, Tillmann N (eds) (2010) Runtime verification\u2014first international conference, proceedings. LNCS, vol 6418. Springer, Berlin"},{"key":"199_CR10","series-title":"LNCS","volume-title":"RV","author":"E Bartocci","year":"2012","unstructured":"Bartocci E, Grosu R, Karmarkar A, Smolka S, Stoller S, Zadok E, Seyster J (2012) Adaptive runtime verification. In: RV. LNCS. Springer, Berlin"},{"key":"199_CR11","series-title":"LNCS","first-page":"260","volume-title":"RV","author":"D Basin","year":"2011","unstructured":"Basin D, Klaedtke F, Z\u0103linescu E (2011) Algorithms for monitoring real-time properties. In: RV. LNCS, vol 7186. Springer, Berlin, pp 260\u2013275"},{"issue":"6","key":"199_CR12","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1093\/comjnl\/44.6.531","volume":"44","author":"I Bate","year":"2001","unstructured":"Bate I, Conmy P, Kelly T, McDermid J (2001) Use of modern processors in safety-critical applications. Comput J 44(6):531\u2013543","journal-title":"Comput J"},{"issue":"3","key":"199_CR13","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"},{"key":"199_CR14","first-page":"125","volume-title":"ICICT","author":"D Borrione","year":"2005","unstructured":"Borrione D, Liu M, Morin-Allory K, Ostier P, Fesquet L (2005) On-line assertion-based verification with proven correct monitors. In: ICICT, pp 125\u2013143"},{"key":"199_CR15","first-page":"221","volume-title":"ICCD","author":"M Boul\u00e9","year":"2005","unstructured":"Boul\u00e9 M, Zilic Z (2005) Incorporating efficient assertion checkers into hardware emulation. In: ICCD. IEEE Computer Society Press, Los Alamitos, pp 221\u2013228"},{"key":"199_CR16","series-title":"Eleventh annual IEEE international","first-page":"69","volume-title":"High-level design validation and test workshop","author":"M Boul\u00e9","year":"2006","unstructured":"Boul\u00e9 M, Zilic Z (2006) Efficient automata-based assertion-checker synthesis of PSL properties. In: High-level design validation and test workshop. Eleventh annual IEEE international, pp 69\u201376"},{"key":"199_CR17","doi-asserted-by":"crossref","unstructured":"Boul\u00e9 M, Zilic Z (2008) Automata-based assertion-checker synthesis of PSL properties. ACM Trans Des Autom Electron Syst 13(1)","DOI":"10.1145\/1297666.1297670"},{"issue":"4","key":"199_CR18","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S1571-0661(04)80575-9","volume":"70","author":"M Br\u00f6rkens","year":"2002","unstructured":"Br\u00f6rkens M, M\u00f6ller M (2002) Dynamic event generation for runtime checking using the JDI. Electron Notes Theor Comput Sci 70(4):21\u201335","journal-title":"Electron Notes Theor Comput Sci"},{"key":"199_CR19","unstructured":"Chenard JS (2011) Hardware-based temporal logic checkers for the debugging of digital integrated circuits. PhD thesis, McGill University"},{"key":"199_CR20","series-title":"ICESS \u201907","doi-asserted-by":"crossref","first-page":"584","DOI":"10.1007\/978-3-540-72685-2_54","volume-title":"Proceedings of the 3rd international conference on embedded software and systems","author":"PH Cheung","year":"2007","unstructured":"Cheung PH, Forin A (2007) A C-language binding for PSL. In: Proceedings of the 3rd international conference on embedded software and systems. ICESS \u201907. Springer, Berlin, pp 584\u2013591"},{"key":"199_CR21","first-page":"3","volume-title":"LICS","author":"EM Clarke","year":"2009","unstructured":"Clarke EM (2009) My 27-year quest to overcome the state explosion problem. In: LICS. IEEE Computer Society Press, Los Alamitos, p 3"},{"key":"199_CR22","isbn-type":"print","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge. ISBN 0262032708","ISBN":"https:\/\/id.crossref.org\/isbn\/0262032708"},{"key":"199_CR23","series-title":"LNCS","first-page":"103","volume-title":"FORMATS","author":"C Colombo","year":"2009","unstructured":"Colombo C, Pace GJ, Schneider G (2009) Safe runtime verification of real-time properties. In: FORMATS. LNCS, vol 5813. Springer, Berlin, pp 103\u2013117"},{"key":"199_CR24","volume-title":"POPL","author":"P Cousot","year":"1977","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL"},{"key":"199_CR25","first-page":"1","volume-title":"DATE","author":"S Das","year":"2006","unstructured":"Das S, Mohanty R, Dasgupta P, Chakrabarti P (2006) Synthesis of system verilog assertions. In: DATE, vol 2, pp 1\u20136"},{"key":"199_CR26","first-page":"35","volume-title":"TIME","author":"S Divakaran","year":"2010","unstructured":"Divakaran S, D\u2019Souza D, Mohan MR (2010) Conflict-tolerant real-time specifications in metric temporal logic. In: TIME, pp 35\u201342"},{"key":"199_CR27","first-page":"IV-748","volume-title":"ISCAS","author":"R Drechsler","year":"2003","unstructured":"Drechsler R (2003) Synthesizing checkers for on-line verification of system-on-chip designs. In: ISCAS, vol 4, pp IV-748\u2013IV-751"},{"key":"199_CR28","first-page":"1316","volume-title":"NPIC&HMIT","author":"A Druilhe","year":"2010","unstructured":"Druilhe A, Daumas F, Nguyen T (2010) Formal verification of an FPGA emulation of the motorola 6800 microprocessor. In: NPIC&HMIT. American Nuclear Society, New York, pp 1316\u20131325"},{"key":"199_CR29","series-title":"LNCS","first-page":"114","volume-title":"CAV","author":"D Drusinsky","year":"2003","unstructured":"Drusinsky D (2003) Monitoring temporal rules combined with time series. In: CAV. LNCS, vol 2725. Springer, Berlin, pp 114\u2013118"},{"key":"199_CR30","series-title":"NASA office of chief engineer","volume-title":"NASA study on flight software complexity","year":"2009","unstructured":"Dvorak D (ed) (2009) NASA study on flight software complexity. NASA office of chief engineer"},{"key":"199_CR31","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1145\/1450058.1450093","volume-title":"EMSOFT","author":"E Eide","year":"2008","unstructured":"Eide E, Regehr J (2008) Volatiles are miscompiled, and what to do about it. In: EMSOFT. ACM, New York, pp 255\u2013264"},{"key":"199_CR32","first-page":"995","volume-title":"Handbook of theoretical computer science, vol B","author":"EA Emerson","year":"1990","unstructured":"Emerson EA (1990) Temporal and modal logic. In: Handbook of theoretical computer science, vol B. MIT Press, Cambridge, pp 995\u20131072"},{"key":"199_CR33","volume-title":"RTSS","author":"J Engblom","year":"2001","unstructured":"Engblom J (2001) On hardware and hardware models for embedded real-time systems. In: RTSS"},{"issue":"4","key":"199_CR34","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1109\/TII.2010.2068304","volume":"6","author":"S Fischmeister","year":"2010","unstructured":"Fischmeister S, Lam P (2010) Time-aware instrumentation of embedded software. IEEE Trans Ind Inform 6(4):652\u2013663","journal-title":"IEEE Trans Ind Inform"},{"key":"199_CR35","series-title":"LNCS","first-page":"188","volume-title":"APLAS","author":"A Flexeder","year":"2010","unstructured":"Flexeder A, Mihaila B, Petter M, Seidl H (2010) Interprocedural control flow reconstruction. In: APLAS. LNCS, vol 6461. Springer, Berlin, pp 188\u2013203"},{"key":"199_CR36","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-9228-4","volume-title":"Assertion-based design","author":"H Foster","year":"2003","unstructured":"Foster H, Lacey D, Krolnik A (2003) Assertion-based design, 2nd edn. Kluwer Academic, Norwell","edition":"2"},{"key":"199_CR37","first-page":"757","volume-title":"CSCS\u201905 international conference on control systems and computer science","author":"S Gheorghita","year":"2005","unstructured":"Gheorghita S, Grigore R (2005) Constructing checkers from PSL properties. In: CSCS\u201905 international conference on control systems and computer science, pp 757\u2013762"},{"key":"199_CR38","series-title":"LNCS","first-page":"200","volume-title":"CHARME 2003","author":"M Gordon","year":"2003","unstructured":"Gordon M, Hurd J, Slind K (2003) Executing the formal semantics of the accellera property specification language by mechanised theorem proving. In: CHARME 2003. LNCS, vol 2860. Springer, Berlin, pp\u00a0200\u2013215"},{"issue":"2","key":"199_CR39","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1023\/B:FORM.0000017721.39909.4b","volume":"24","author":"K Havelund","year":"2004","unstructured":"Havelund K, Ro\u015fu G (2004) An overview of the runtime verification tool Java PathExplorer. Form Methods Syst Des 24(2):189\u2013215","journal-title":"Form Methods Syst Des"},{"key":"199_CR40","first-page":"7","volume-title":"TestCom\/FATES","author":"K Havelund","year":"2008","unstructured":"Havelund K (2008) Runtime verification of C programs. In: TestCom\/FATES. Springer, Berlin, pp 7\u201322"},{"key":"199_CR41","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K Havelund","year":"2004","unstructured":"Havelund K, Ro\u015fu G (2004) Efficient monitoring of safety properties. Int J Softw Tools Technol Transf 6:158\u2013173","journal-title":"Int J Softw Tools Technol Transf"},{"key":"199_CR42","series-title":"LNCS","first-page":"342","volume-title":"TACAS","author":"K Havelund","year":"2002","unstructured":"Havelund K, Rosu G (2002) Synthesizing monitors for safety properties. In: TACAS. LNCS. Springer, Berlin, pp 342\u2013356"},{"key":"199_CR43","volume-title":"Introduction to automata theory, languages, and computation","author":"JE Hopcroft","year":"2006","unstructured":"Hopcroft JE, Motwani R, Ullman JD (2006) Introduction to automata theory, languages, and computation. Addison-Wesley Longman, Reading"},{"key":"199_CR44","isbn-type":"print","volume-title":"The art of electronics","author":"P Horowitz","year":"1980","unstructured":"Horowitz P, Hill W (1980) The art of electronics. Cambridge University Press, Cambridge. ISBN 0521370957","ISBN":"https:\/\/id.crossref.org\/isbn\/0521370957"},{"key":"199_CR45","series-title":"LNCS","first-page":"306","volume-title":"ATVA","author":"J Howe","year":"2009","unstructured":"Howe J, King A (2009) Logahedra: a new weakly relational domain. In: ATVA. LNCS, vol 5799. Springer, Berlin, pp 306\u2013320"},{"key":"199_CR46","series-title":"LNCS","first-page":"214","volume-title":"VMCAI","author":"J Kinder","year":"2009","unstructured":"Kinder J, Veith H, Zuleger F (2009) An abstract interpretation-based framework for control flow reconstruction from binaries. In: VMCAI. LNCS, vol 5403. Springer, Berlin, pp 214\u2013228"},{"issue":"8","key":"199_CR47","doi-asserted-by":"crossref","first-page":"786","DOI":"10.1109\/TC.1973.5009159","volume":"22","author":"PM Kogge","year":"1973","unstructured":"Kogge PM, Stone HS (1973) A parallel algorithm for the efficient solution of a general class of recurrence equations. IEEE Trans Comput 22(8):786\u2013793","journal-title":"IEEE Trans Comput"},{"key":"199_CR48","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8237-7","volume-title":"Real-time systems","author":"H Kopetz","year":"2011","unstructured":"Kopetz H (2011) Real-time systems, 2nd edn. Springer, Berlin","edition":"2"},{"key":"199_CR49","volume-title":"Decision procedures: an algorithmic point of view","author":"D Kroening","year":"2008","unstructured":"Kroening D, Strichman O (2008) Decision procedures: an algorithmic point of view. Springer, Berlin"},{"key":"199_CR50","first-page":"383","volume-title":"LICS","author":"F Laroussinie","year":"2002","unstructured":"Laroussinie F, Markey N, Schnoebelen P (2002) Temporal logic with forgettable past. In: LICS. IEEE, New York, pp 383\u2013392"},{"key":"199_CR51","first-page":"279","volume-title":"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: PDPTA, pp 279\u2013287"},{"key":"199_CR52","first-page":"42","volume-title":"POPL","author":"X Leroy","year":"2006","unstructured":"Leroy X (2006) Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL. ACM, New York, pp 42\u201354"},{"key":"199_CR53","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy X (2009) A formally verified compiler back-end. J Autom Reason 43:363\u2013446","journal-title":"J Autom Reason"},{"key":"199_CR54","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logics of programs","author":"O Lichtenstein","year":"1985","unstructured":"Lichtenstein O, Pnueli A, Zuck L (1985) The glory of the past. In: Logics of programs. LNCS, vol 193. Springer, Berlin, pp 196\u2013218"},{"key":"199_CR55","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/1085130.1085132","volume-title":"AADEBUG","author":"C Lindig","year":"2005","unstructured":"Lindig C (2005) Random testing of C calling conventions. In: AADEBUG. ACM, New York, pp 3\u201312"},{"key":"199_CR56","unstructured":"Lu H, Forin A (2007) The design and implementation of P2V, an architecture for zero-overhead online verification of software programs. Tech rep MSR-TR-2007-99, Microsoft Research"},{"key":"199_CR57","first-page":"2","volume-title":"FORMATS","author":"O Maler","year":"2005","unstructured":"Maler O, Nickovic D, Pnueli A (2005) Real time temporal logic: past, present, future. In: FORMATS, pp 2\u201316"},{"key":"199_CR58","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems","author":"Z Manna","year":"1992","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems. Springer, Berlin"},{"key":"199_CR59","isbn-type":"print","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-007-0257-8","volume-title":"Embedded system design","author":"P Marwedel","year":"2011","unstructured":"Marwedel P (2011) Embedded system design. Springer, Berlin. ISBN 9789400702578","ISBN":"https:\/\/id.crossref.org\/isbn\/9789400702578"},{"key":"199_CR60","first-page":"1","volume-title":"DATE","author":"K Morin-Allory","year":"2006","unstructured":"Morin-Allory K, Borrione D (2006) Proven correct monitors from PSL specifications. In: DATE, pp 1\u20136"},{"key":"199_CR61","doi-asserted-by":"crossref","first-page":"789","DOI":"10.1002\/spe.4380250705","volume":"25","author":"TJ Parr","year":"1995","unstructured":"Parr TJ, Quong RW (1995) ANTLR: a predicated-ll(k) parser generator. Softw Pract Exp 25:789\u2013810","journal-title":"Softw Pract Exp"},{"key":"199_CR62","first-page":"481","volume-title":"RTSS","author":"R Pellizzoni","year":"2008","unstructured":"Pellizzoni R, Meredith P, Caccamo M, Rosu G (2008) Hardware runtime monitoring for dependable COTS-based real-time embedded systems. In: RTSS, pp 481\u2013491"},{"key":"199_CR63","first-page":"481","volume-title":"RTSS","author":"R Pellizzoni","year":"2008","unstructured":"Pellizzoni R, Meredith P, Caccamo M, Rosu G (2008) Hardware runtime monitoring for dependable COTS-based real-time embedded systems. In: RTSS, pp 481\u2013491"},{"key":"199_CR64","series-title":"LNCS","first-page":"345","volume-title":"RV","author":"L Pike","year":"2010","unstructured":"Pike L, Goodloe A, Morisset R, Niller S (2010) Copilot: a hard real-time runtime monitor. In: RV. LNCS, vol 6418. Springer, Berlin, pp 345\u2013359"},{"key":"199_CR65","series-title":"LNCS","first-page":"310","volume-title":"RV","author":"L Pike","year":"2011","unstructured":"Pike L, Niller S, Wegmann N (2011) Runtime verification for ultra-critical systems. In: RV. LNCS, vol 7186. Springer, Berlin, pp 310\u2013324"},{"key":"199_CR66","volume-title":"Proceedings of the 2nd Euromicro international workshop on WCET analysis","author":"P Puschner","year":"2002","unstructured":"Puschner P (2002) Is worst-case execution-time analysis a non-problem? \u2013 towards new software and hardware architectures. In: Proceedings of the 2nd Euromicro international workshop on WCET analysis, Department of Computer Science, University of York"},{"key":"199_CR67","first-page":"117","volume-title":"EMSOFT","author":"T Reinbacher","year":"2011","unstructured":"Reinbacher T, Brauer J (2011) Precise control flow reconstruction using boolean logic. In: EMSOFT. ACM, New York, pp 117\u2013126"},{"key":"199_CR68","series-title":"LNCS","first-page":"37","volume-title":"FMICS","author":"T Reinbacher","year":"2011","unstructured":"Reinbacher T, Brauer J, Horauer M, Steininger A, Kowalewski S (2011) Past time LTL runtime verification for microcontroller binary code. In: FMICS. LNCS, vol 6959. Springer, Berlin, pp 37\u201351"},{"key":"199_CR69","doi-asserted-by":"crossref","unstructured":"Reinbacher T, Brauer J, Horauer M, Steininger A, Kowalewski S (2012) Runtime verification of microcontroller binary code. Sci Comput Program (in press)","DOI":"10.1007\/978-3-642-24431-5_5"},{"key":"199_CR70","series-title":"LNCS","first-page":"239","volume-title":"RV","author":"T Reinbacher","year":"2011","unstructured":"Reinbacher T, Brauer J, Schachinger D, Steininger A, Kowalewski S (2011) Automated test-trace inspection for microcontroller binary code. In: RV. LNCS, vol 7186. Springer, Berlin, pp 239\u2013244"},{"key":"199_CR71","series-title":"LNCS","first-page":"110","volume-title":"RV","author":"T Reinbacher","year":"2013","unstructured":"Reinbacher T, F\u00fcgger M, Brauer J (2013) Real-time runtime verification on chip. In: Qadeer S, Tasiran\u00a0S (eds) RV. LNCS, vol 7687. Springer, Berlin, pp 110\u2013125"},{"issue":"2","key":"199_CR72","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/s10515-005-6205-y","volume":"12","author":"G Ro\u015fu","year":"2005","unstructured":"Ro\u015fu G, Havelund K (2005) Rewriting-based techniques for runtime verification. Autom Softw Eng 12(2):151\u2013197","journal-title":"Autom Softw Eng"},{"key":"199_CR73","unstructured":"RTCA\/DO-178B (1992) Software considerations in airborne systems and equipment certification"},{"key":"199_CR74","series-title":"LNCS","first-page":"399","volume-title":"RV","author":"J Schumann","year":"2010","unstructured":"Schumann J, Srivastava A, Mengshoel O (2010) Who guards the guardians? Toward V&V of health management software. In: RV. LNCS, vol 6418, pp 399\u2013404"},{"key":"199_CR75","first-page":"335","volume-title":"FMCAD","author":"K Shimizu","year":"2000","unstructured":"Shimizu K, Dill DL, Hu AJ (2000) Monitor-based formal specification of PCI. In: FMCAD. Springer, Berlin, pp 335\u2013353"},{"key":"199_CR76","first-page":"320","volume-title":"CSE","author":"M Straka","year":"2008","unstructured":"Straka M, Kot\u00e1sek Z, Winter J (2008) The design of hardware checkers for verification and diagnostic purposes. In: CSE, pp 320\u2013327"},{"issue":"3","key":"199_CR77","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/s10703-011-0139-8","volume":"41","author":"D Tabakov","year":"2012","unstructured":"Tabakov D, Rozier KY, Vardi MY (2012) Optimized temporal monitors for SystemC. Form Methods Syst Des 41(3):236\u2013268","journal-title":"Form Methods Syst Des"},{"key":"199_CR78","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/j.entcs.2004.01.029","volume":"113","author":"P Thati","year":"2005","unstructured":"Thati P, Ro\u015fu G (2005) Monitoring algorithms for metric temporal logic specifications. Electron Notes Theor Comput Sci 113:145\u2013162","journal-title":"Electron Notes Theor Comput Sci"},{"key":"199_CR79","doi-asserted-by":"crossref","first-page":"897","DOI":"10.1109\/32.57626","volume":"16","author":"JJP Tsai","year":"1990","unstructured":"Tsai JJP, Fang KY, Chen HY, Bi Y (1990) A noninterference monitoring and replay mechanism for real-time software testing and debugging. IEEE Trans Softw Eng 16:897\u2013916","journal-title":"IEEE Trans Softw Eng"},{"issue":"5","key":"199_CR80","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1049\/iet-sen:20060076","volume":"1","author":"C Watterson","year":"2007","unstructured":"Watterson C, Heffernan D (2007) Runtime verification and monitoring of embedded systems. IET Softw 1(5):172\u2013179","journal-title":"IET Softw"},{"key":"199_CR81","first-page":"283","volume-title":"PLDI","author":"X Yang","year":"2011","unstructured":"Yang X, Chen Y, Eide E, Regehr J (2011) Finding and understanding bugs in C compilers. In: PLDI. ACM, New York, pp 283\u2013294"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0199-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0199-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0199-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,1]],"date-time":"2019-08-01T02:38:37Z","timestamp":1564627117000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0199-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11,7]]},"references-count":81,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,6]]}},"alternative-id":["199"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0199-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,11,7]]}}}