×

zbMATH — the first resource for mathematics

Runtime verification of embedded real-time systems. (English) Zbl 1317.68122
Summary: We present a runtime verification framework that allows on-line monitoring of past-time Metric Temporal Logic (ptMTL) specifications in a discrete time setting. We design observer algorithms for the time-bounded modalities of ptMTL, which take advantage of the highly parallel nature of hardware designs. The algorithms can be translated into efficient hardware blocks, which are designed for reconfigurability, thus, facilitate applications of the framework in both a prototyping and a post-deployment phase of embedded real-time systems. We provide formal correctness proofs for all presented observer algorithms and analyze their time and space complexity. For example, for the most general operator considered, the time-bounded Since operator, we obtain a time complexity that is doubly logarithmic both in the point in time the operator is executed and the operator’s time bounds. This result is promising with respect to a self-contained, non-interfering monitoring approach that evaluates real-time specifications in parallel to the system-under-test. We implement our framework on a Field Programmable Gate Array platform and use extensive simulation and logic synthesis runs to assess the benefits of the approach in terms of resource usage and operating frequency.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68W27 Online algorithms; streaming algorithms
Software:
ANTLR; Copilot; FoCs; JPAX
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abarbanel, Y; Beer, I; Gluhovsky, L; Keidar, S; Wolfsthal, Y, Focs: automatic generation of simulation checkers from formal specifications, No. 1855, 538-542, (2000), Berlin · Zbl 0974.68552
[2] Alur, R; Henzinger, TA, Real-time logics: complexity and expressiveness, 390-401, (1990), New York
[3] 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, The forspec temporal logic: a new temporal property-specification language, 196-211, (2002), Berlin · Zbl 1043.68563
[4] Armoni, R; Korchemny, D; Tiemeyer, A; Vardi, M; Zbar, Y, Deterministic dynamic monitors for linear-time assertions, No. 4262, 163-177, (2006), Berlin
[5] Austin, TM, DIVA: a reliable substrate for deep submicron microarchitecture design, 196-207, (1999), New York
[6] Baier C, Katoen JP (2008) Principles of model checking. MIT Press, Cambridge · Zbl 1179.68076
[7] Bardin, S; Herrmann, P; Védrine, F, Refinement-based CFG reconstruction from unstructured programs, 54-69, (2011), Berlin · Zbl 1317.68028
[8] Barre, B; Klein, M; Soucy-Boivin, M; Ollivier, PA; Hallé, S, Mapreduce for parallel trace validation of LTL properties, (2012), Berlin
[9] Barringer H, Falcone Y, Finkbeiner B, Havelund K, Lee I, Pace GJ, Rosu G, Sokolsky O, Tillmann N (eds) (2010) Runtime verification—first international conference, proceedings. LNCS, vol 6418. Springer, Berlin
[10] Bartocci, E; Grosu, R; Karmarkar, A; Smolka, S; Stoller, S; Zadok, E; Seyster, J, Adaptive runtime verification, (2012), Berlin
[11] Basin, D; Klaedtke, F; Zălinescu, E, Algorithms for monitoring real-time properties, No. 7186, 260-275, (2011), Berlin
[12] Bate, I; Conmy, P; Kelly, T; McDermid, J, Use of modern processors in safety-critical applications, Comput J, 44, 531-543, (2001) · Zbl 1027.68513
[13] Bauer, A; Leucker, M; Schallhart, C, Comparing LTL semantics for runtime verification, J Log Comput, 20, 651-674, (2010) · Zbl 1213.68363
[14] Borrione, D; Liu, M; Morin-Allory, K; Ostier, P; Fesquet, L, On-line assertion-based verification with proven correct monitors, 125-143, (2005)
[15] Boulé, M; Zilic, Z, Incorporating efficient assertion checkers into hardware emulation, 221-228, (2005), Los Alamitos
[16] Boulé, M; Zilic, Z, Efficient automata-based assertion-checker synthesis of PSL properties, 69-76, (2006)
[17] Boulé M, Zilic Z (2008) Automata-based assertion-checker synthesis of PSL properties. ACM Trans Des Autom Electron Syst 13(1)
[18] Brörkens, M; Möller, M, Dynamic event generation for runtime checking using the JDI, Electron Notes Theor Comput Sci, 70, 21-35, (2002)
[19] Chenard JS (2011) Hardware-based temporal logic checkers for the debugging of digital integrated circuits. PhD thesis, McGill University · Zbl 1175.03009
[20] Cheung, PH; Forin, A, A C-language binding for PSL, 584-591, (2007), Berlin
[21] Clarke, EM, My 27-year quest to overcome the state explosion problem, 3, (2009), Los Alamitos
[22] Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge. ISBN 0262032708
[23] Colombo, C; Pace, GJ; Schneider, G, Safe runtime verification of real-time properties, No. 5813, 103-117, (2009), Berlin · Zbl 1262.68111
[24] Cousot, P; Cousot, R, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (1977) · Zbl 0788.68094
[25] Das, S; Mohanty, R; Dasgupta, P; Chakrabarti, P, Synthesis of system verilog assertions, No. 2, 1-6, (2006)
[26] Divakaran, S; D’Souza, D; Mohan, MR, Conflict-tolerant real-time specifications in metric temporal logic, 35-42, (2010)
[27] Drechsler, R, Synthesizing checkers for on-line verification of system-on-chip designs, No. 4, iv-748-iv-751, (2003)
[28] Druilhe, A; Daumas, F; Nguyen, T, Formal verification of an FPGA emulation of the motorola 6800 microprocessor, 1316-1325, (2010), New York
[29] Drusinsky, D, Monitoring temporal rules combined with time series, No. 2725, 114-118, (2003), Berlin
[30] Dvorak D (ed) (2009) NASA study on flight software complexity. NASA office of chief engineer
[31] Eide, E; Regehr, J, Volatiles are miscompiled, and what to do about it, 255-264, (2008), New York
[32] Emerson, EA, Temporal and modal logic, 995-1072, (1990), Cambridge · Zbl 0900.03030
[33] Engblom, J, On hardware and hardware models for embedded real-time systems, (2001)
[34] Fischmeister, S; Lam, P, Time-aware instrumentation of embedded software, IEEE Trans Ind Inform, 6, 652-663, (2010)
[35] Flexeder, A; Mihaila, B; Petter, M; Seidl, H, Interprocedural control flow reconstruction, No. 6461, 188-203, (2010), Berlin
[36] Foster H, Lacey D, Krolnik A (2003) Assertion-based design, 2nd edn. Kluwer Academic, Norwell
[37] Gheorghita, S; Grigore, R, Constructing checkers from PSL properties, 757-762, (2005)
[38] Gordon, M; Hurd, J; Slind, K, Executing the formal semantics of the accellera property specification language by mechanised theorem proving, No. 2860, 200-215, (2003), Berlin · Zbl 1179.68085
[39] Havelund, K; Roşu, G, An overview of the runtime verification tool Java pathexplorer, Form Methods Syst Des, 24, 189-215, (2004) · Zbl 1073.68549
[40] Havelund, K, Runtime verification of C programs, 7-22, (2008), Berlin
[41] Havelund, K; Roşu, G, Efficient monitoring of safety properties, Int J Softw Tools Technol Transf, 6, 158-173, (2004)
[42] Havelund, K; Rosu, G, Synthesizing monitors for safety properties, 342-356, (2002), Berlin · Zbl 1043.68534
[43] Hopcroft JE, Motwani R, Ullman JD (2006) Introduction to automata theory, languages, and computation. Addison-Wesley Longman, Reading
[44] Horowitz P, Hill W (1980) The art of electronics. Cambridge University Press, Cambridge. ISBN 0521370957
[45] Howe, J; King, A, Logahedra: a new weakly relational domain, No. 5799, 306-320, (2009), Berlin · Zbl 1262.68122
[46] Kinder, J; Veith, H; Zuleger, F, An abstract interpretation-based framework for control flow reconstruction from binaries, No. 5403, 214-228, (2009), Berlin · Zbl 1206.68091
[47] Kogge, PM; Stone, HS, A parallel algorithm for the efficient solution of a general class of recurrence equations, IEEE Trans Comput, 22, 786-793, (1973) · Zbl 0262.68015
[48] Kopetz H (2011) Real-time systems, 2nd edn. Springer, Berlin · Zbl 1226.68001
[49] Kroening D, Strichman O (2008) Decision procedures: an algorithmic point of view. Springer, Berlin · Zbl 1149.68071
[50] Laroussinie, F; Markey, N; Schnoebelen, P, Temporal logic with forgettable past, 383-392, (2002), New York
[51] Lee, I; Kannan, S; Kim, M; Sokolsky, O; Viswanathan, M, Runtime assurance based on formal specifications, 279-287, (1999)
[52] Leroy, X, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, 42-54, (2006), New York · Zbl 1369.68124
[53] Leroy, X, A formally verified compiler back-end, J Autom Reason, 43, 363-446, (2009) · Zbl 1185.68215
[54] Lichtenstein, O; Pnueli, A; Zuck, L, The glory of the past, No. 193, 196-218, (1985), Berlin · Zbl 0586.68028
[55] Lindig, C, Random testing of C calling conventions, 3-12, (2005), New York
[56] 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
[57] Maler, O; Nickovic, D; Pnueli, A, Real time temporal logic: past, present, future, 2-16, (2005) · Zbl 1175.03009
[58] Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems. Springer, Berlin · Zbl 0753.68003
[59] Marwedel P (2011) Embedded system design. Springer, Berlin. ISBN 9789400702578 · Zbl 1213.68003
[60] Morin-Allory, K; Borrione, D, Proven correct monitors from PSL specifications, 1-6, (2006)
[61] Parr, TJ; Quong, RW, ANTLR: a predicated-ll(k) parser generator, Softw Pract Exp, 25, 789-810, (1995)
[62] Pellizzoni, R; Meredith, P; Caccamo, M; Rosu, G, Hardware runtime monitoring for dependable COTS-based real-time embedded systems, 481-491, (2008)
[63] Pellizzoni, R; Meredith, P; Caccamo, M; Rosu, G, Hardware runtime monitoring for dependable COTS-based real-time embedded systems, 481-491, (2008)
[64] Pike, L; Goodloe, A; Morisset, R; Niller, S, Copilot: a hard real-time runtime monitor, No. 6418, 345-359, (2010), Berlin
[65] Pike, L; Niller, S; Wegmann, N, Runtime verification for ultra-critical systems, No. 7186, 310-324, (2011), Berlin
[66] Puschner, P, Is worst-case execution-time analysis a non-problem? - towards new software and hardware architectures, Department of Computer Science, University of York
[67] Reinbacher, T; Brauer, J, Precise control flow reconstruction using Boolean logic, 117-126, (2011), New York
[68] Reinbacher, T; Brauer, J; Horauer, M; Steininger, A; Kowalewski, S, Past time LTL runtime verification for microcontroller binary code, No. 6959, 37-51, (2011), Berlin
[69] Reinbacher T, Brauer J, Horauer M, Steininger A, Kowalewski S (2012) Runtime verification of microcontroller binary code. Sci Comput Program (in press) · Zbl 06904237
[70] Reinbacher, T; Brauer, J; Schachinger, D; Steininger, A; Kowalewski, S, Automated test-trace inspection for microcontroller binary code, No. 7186, 239-244, (2011), Berlin
[71] Reinbacher, T; Függer, M; Brauer, J; Qadeer, S (ed.); Tasiran, S (ed.), Real-time runtime verification on chip, No. 7687, 110-125, (2013), Berlin
[72] Roşu, G; Havelund, K, Rewriting-based techniques for runtime verification, Autom Softw Eng, 12, 151-197, (2005)
[73] RTCA/DO-178B (1992) Software considerations in airborne systems and equipment certification · Zbl 1175.03009
[74] Schumann, J; Srivastava, A; Mengshoel, O, Who guards the guardians? toward V&V of health management software, No. 6418, 399-404, (2010)
[75] Shimizu, K; Dill, DL; Hu, AJ, Monitor-based formal specification of PCI, 335-353, (2000), Berlin
[76] Straka, M; Kotásek, Z; Winter, J, The design of hardware checkers for verification and diagnostic purposes, 320-327, (2008)
[77] Tabakov, D; Rozier, KY; Vardi, MY, Optimized temporal monitors for systemc, Form Methods Syst Des, 41, 236-268, (2012) · Zbl 1284.68206
[78] Thati, P; Roşu, G, Monitoring algorithms for metric temporal logic specifications, Electron Notes Theor Comput Sci, 113, 145-162, (2005)
[79] Tsai, JJP; Fang, KY; Chen, HY; Bi, Y, A noninterference monitoring and replay mechanism for real-time software testing and debugging, IEEE Trans Softw Eng, 16, 897-916, (1990)
[80] Watterson, C; Heffernan, D, Runtime verification and monitoring of embedded systems, IET Softw, 1, 172-179, (2007)
[81] Yang, X; Chen, Y; Eide, E; Regehr, J, Finding and understanding bugs in C compilers, 283-294, (2011), New York
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.