×

zbMATH — the first resource for mathematics

Optimized temporal monitors for SystemcC. (English) Zbl 1284.68206
Summary: SystemC is a modeling language built as an extension of C++. Its growing popularity and the increasing complexity of designs have motivated research efforts aimed at the verification of SystemC models using assertion-based verification (ABV), where the designer asserts properties that capture the design intent in a formal language such as PSL or SVA. The model then can be verified against the properties using runtime or formal verification techniques. In this paper we focus on automated generation of runtime monitors from temporal properties. Our focus is on minimizing runtime overhead, rather than monitor size or monitor-generation time. We identify four issues in monitor generation: state minimization, alphabet representation, alphabet minimization, and monitor encoding. We conduct extensive experimentation and identify a combination of settings that offers the best performance in terms of runtime overhead.

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N15 Theory of programming languages
68P30 Coding and information theory (compaction, compression, models of communication, encoding schemes, etc.) (aspects in computer science)
Software:
Java-MOP; FoCs; z3; SPOT
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abarbanel Y, Beer I, Gluhovsky L, Keidar S, Wolfsthal Y (2000) Focs: Automatic generation of simulation checkers from formal specifications. In: CAV’00: Proc of the 12th international conference on computer aided verification, pp 538–542 · Zbl 0974.68552
[2] Armoni R, Korchemny D, Tiemeyer A, Vardi M, Zbar Y (2006) Deterministic dynamic monitors for linear-time assertions. In: Proc workshop on formal approaches to testing and runtime verification. LNCS, vol 4262. Springer, Berlin
[3] Bauer A, Leucker M, Schallhart C (2006) Monitoring of real-time properties. In: FSTTCS’06: Foundations of software technology and theoretical computer science, 26th international conference. LNCS, vol 4337. Springer, Berlin, pp 260–272 · Zbl 1177.68141
[4] Bodden E, Hendren LJ, Lam P, Lhoták O, Naeem NA (2010) Collaborative runtime verification with tracematches. J Log Comput 20(3):707–723 · Zbl 1213.68365
[5] Boulé M, Zilic Z (2008) Generating hardware assertion checkers. Springer, Berlin
[6] Bryant R (1986) Graph-based algorithms for Boolean-function manipulation. IEEE Trans Comput C-35(8) · Zbl 0593.94022
[7] Bryant R (1992) Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293–318
[8] Bunker A, Gopalakrishnan G, McKee SA (2004) Formal hardware specification languages for protocol compliance verification. ACM Trans Des Autom Electron Syst 9(1):1–32 · Zbl 05456735
[9] Bustan D, Fisman D, Havlicek J (2005) Automata construction for PSL. Tech Rep, The Weizmann Institute of Science
[10] Chang H, Cooke L, Hunt M, Martin G, McNelly AJ, Todd L (1999) Surviving the SOC revolution: a guide to platform-based design. Kluwer Academic, Norwell
[11] Chen F, Jin D, Meredith P, Roşu G (2009) Monitoring oriented programming–a project overview. In: Proceedings of the fourth international conference on intelligent computing and information systems (ICICIS’09). ACM, New York, pp 72–77
[12] Cooper KD, Torczon L (2004) Engineering a compiler. Morgan Kaufmann, San Mateo · Zbl 1058.68036
[13] Courcoubetis C, Vardi M, Wolper P, Yannakakis M (1992) Memory efficient algorithms for the verification of temporal properties. Form Methods Syst Des 1:275–288 · Zbl 0786.68060
[14] d’Amorim M, Rosu G (2005) Efficient monitoring of {\(\omega\)}-languages. In: Proc 17th international conference on computer aided verification, pp 364–378
[15] Daniele M, Giunchiglia F, Vardi MY (1999) Improved automata generation for linear temporal logic. In: CAV’99: Proc 11th int conf on computer aided verification. Springer, London, pp 249–260 · Zbl 1046.68588
[16] Duret-Lutz A, Poitrenaud D (2004) SPOT: An extensible model checking library using transition-based generalized Büchi automata. Modeling Anal Simul Comput Syst. doi: 10.1109/MASCOT.2004.1348184
[17] Eisner C, Fisman D (2006) A practical introduction to PSL. Springer, New York
[18] Finkbeiner B, Sipma H (2004) Checking finite traces using alternating automata. Form Methods Syst Des 24(2):101–127. doi: 10.1023/B:FORM.0000017718.28096.48 · Zbl 1073.68053
[19] Geilen M (2001) On the construction of monitors for temporal logic properties. Electr Notes Theor Comput Sci 55(2)
[20] Geist D, Biran G, Arons T, Slavkin M, Nustov Y, Farkas M, Holtz K, Long A, King D, Barret S (1999) A methodology for the verification of a ”system on chip”. In: DAC’99: Proc 36th design automation conference. ACM, New York, pp 574–579. doi: 10.1145/309847.310001
[21] Geldenhuys J, Hansen H (2006) Larger automata and less work for LTL model checking. In: Model checking software, 13th int SPIN workshop. LNCS, vol 3925. Springer, Berlin, pp 53–70 · Zbl 1178.68343
[22] Gerth R, Peled D, Vardi M, Wolper P (1995) Simple on-the-fly automatic verification of Linear Temporal Logic. In: Dembiski P, Sredniawa M (eds) Protocol specification, testing, and verification. Chapman & Hall, London, pp 3–18
[23] Giannakopoulou D, Havelund K (2001) Automata-based verification of temporal properties on running programs. In: Int conf on automated software engineering. IEEE, Washington, p 412
[24] Grotker T, Liao S, Martin G, Swan S (2002) System design with SystemC. Kluwer Academic, Norwell
[25] IEEE working group (2007) Standard for property specification language (PSL). IEC 62531:2007 (E), pp 1–156. doi: 10.1109/IEEESTD.2007.4408637
[26] Gupta A (2002) Assertion-based verification turns the corner. IEEE Des Test Comput 19:131–132. doi: 10.1109/MDT.2002.10025
[27] Hoos HH (2008) Computer-aided design of high-performance algorithms. Tech rep, University of British Columbia
[28] Hopcroft J, Ullman J (1979) Introduction to automata theory, languages, and computation. Addison-Wesley, Reading · Zbl 0426.68001
[29] Jard C, Jeron T (1989) On-line model-checking for finite linear temporal logic specifications. In: Automatic verification methods for finite state systems, Proc international workshop, Grenoble. LNCS, vol 407. Springer, Grenoble, pp 189–196
[30] Jin D, Meredith P, Griffith D, Roşu G (2011) Garbage collection for monitoring parametric properties. In: Programming language design and implementation (PLDI’11). ACM, New York, pp 415–424. doi: 10.1145/1993316.1993547
[31] Kupferman O, Lampert R (2006) On the construction of fine automata for safety properties. In: ATVA’06: Proc of the international symposium on automated technology for verification and analysis, pp 110–124 · Zbl 1161.68572
[32] Kupferman O, Vardi M (2001) Model checking of safety properties. Form Methods Syst Des 19(3):291–314 · Zbl 0995.68061
[33] Meredith P, Jin D, Griffith D, Chen F, Roşu G (2011) An overview of the MOP runtime verification framework. Int J Softw Tech Technol Transfer. doi: 10.1007/s10009-011-0198-6
[34] Møller A (2004) http://www.brics.dk/automaton/
[35] Morin-Allory K, Borrione D (2006) Proven correct monitors from PSL specifications. In: DATE’06: Proc conf on design, automation and test in Europe, European Design and Automation Association, pp 1246–1251
[36] de Moura LM, Bjørner N (2008) Z3: An efficient SMT solver. In: TACAS’08: Tools and algorithms for the construction and analysis of systems, 14th international conference, pp 337–340
[37] Pierre L, Ferro L (2008) A tractable and fast method for monitoring SystemC TLM specifications. IEEE Trans Comput 57:1346–1356. doi: 10.1109/TC.2008.74
[38] Rönkkö M (2011) LBT: LTL to Büchi conversion. Available online (1999). http://www.tcs.hut.fi/Software/maria/tools/lbt/ . Accessed March 29, 2011
[39] Rozier KY, Vardi MY (2007) LTL satisfiability checking. In: Proc 14th int SPIN conference on model checking software. Springer, Berlin, pp 149–167
[40] Stolz V, Bodden E (2006) Temporal assertions using AspectJ. Electron Notes Theor Comput Sci 144(4):109–124. doi: 10.1016/j.entcs.2006.02.007
[41] Tabakov D, Vardi M (2010) Monitoring temporal SystemC properties. In: Proc 8th int’l conf on formal methods and models for codesign. IEEE, New York, pp 123–132
[42] Tabakov D, Vardi M, Kamhi G, Singerman E (2008) A temporal language for SystemC. In: FMCAD’08: Proc int conf on formal methods in computer-aided design. IEEE Press, New York, pp 1–9. http://portal.acm.org/citation.cfm?id=1517446
[43] Tabakov D, Vardi MY (2005) Experimental evaluation of classical automata constructions. In: LPAR’05: 12th int conf on logic for programming, artificial intelligence, and reasoning, pp 396–411 · Zbl 1143.68443
[44] Vardi M, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1–37 · Zbl 0827.03009
[45] Vijayaraghavan S, Ramanathan M (2005) A practical guide for SystemVerilog assertions. Springer, 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.