Skip to main content
SpringerLink
Log in

Optimized temporal monitors for SystemC

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Listing 1
Listing 2
Fig. 1
Fig. 2
Listing 3
Listing 4
Fig. 3
Listing 5
Listing 6
Listing 7
Listing 8
Listing 9
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15

Similar content being viewed by others

Notes

  1. IEEE Standard 1666–2005.

  2. Property Specification Language, IEEE Standard 1850–2007.

  3. SystemVerilog Assertions, IEEE Standard 1800–2005.

  4. Note that the comparison is between different monitor implementations and is applicable to other C or C++ modeling languages.

  5. BRICS Automaton represents the alphabet of the automaton as Unicode characters, which have one-to-one correspondence to the set of 16-bit integers.

  6. Source code available at http://www.cs.rice.edu/CS/Verification/Software/software.html.

  7. http://www.cs.rice.edu/CS/Verification/Software/software.html.

  8. http://www.rcsg.rice.edu/ada.

  9. http://rcsg.rice.edu/sugar/.

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

    Chapter  Google Scholar 

  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

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Article  MATH  Google Scholar 

  5. Boulé M, Zilic Z (2008) Generating hardware assertion checkers. Springer, Berlin

    Book  Google Scholar 

  6. Bryant R (1986) Graph-based algorithms for Boolean-function manipulation. IEEE Trans Comput C-35(8)

  7. Bryant R (1992) Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293–318

    Article  Google Scholar 

  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

    Article  Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  12. Cooper KD, Torczon L (2004) Engineering a compiler. Morgan Kaufmann, San Mateo

    Google Scholar 

  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

    Article  Google Scholar 

  14. d’Amorim M, Rosu G (2005) Efficient monitoring of ω-languages. In: Proc 17th international conference on computer aided verification, pp 364–378

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Google Scholar 

  17. Eisner C, Fisman D (2006) A practical introduction to PSL. Springer, New York

    Google Scholar 

  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

    Article  MATH  Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  24. Grotker T, Liao S, Martin G, Swan S (2002) System design with SystemC. Kluwer Academic, Norwell

    Google Scholar 

  25. IEEE working group (2007) Standard for property specification language (PSL). IEC 62531:2007 (E), pp 1–156. doi:10.1109/IEEESTD.2007.4408637

    Google Scholar 

  26. Gupta A (2002) Assertion-based verification turns the corner. IEEE Des Test Comput 19:131–132. doi:10.1109/MDT.2002.10025

    Google Scholar 

  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

    MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Google Scholar 

  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

    Chapter  Google Scholar 

  32. Kupferman O, Vardi M (2001) Model checking of safety properties. Form Methods Syst Des 19(3):291–314

    Article  MathSciNet  MATH  Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Article  MathSciNet  Google Scholar 

  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

    Google Scholar 

  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

    Article  Google Scholar 

  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

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  44. Vardi M, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1–37

    Article  MathSciNet  MATH  Google Scholar 

  45. Vijayaraghavan S, Ramanathan M (2005) A practical guide for SystemVerilog assertions. Springer, New York

    Google Scholar 

Download references

Acknowledgements

We thank Alexandre Duret-Lutz for his code patch replacing the functionality of spot::prune_scc, which we used to upgrade from SPOT 0.4, used in the experiments executed on Ada, to SPOT 0.7.1 used in the experiments executed on SUG@R. We also thank Patrick Meredith and Dmitry Korchemny for suggesting that we consider table look-up encodings. Finally, we thank the anonymous reviewers for their comments and feedback.

Author information

Authors and Affiliations

  1. Schlumberger Information Solutions, 5599 San Felipe Str. #100, Houston, TX, 77056, USA

    Deian Tabakov

  2. NASA Ames Research Center, Moffett Field, CA, 94035, USA

    Kristin Y. Rozier

  3. Rice University, 6100 Main Str. MS-132, Houston, TX, 77005, USA

    Moshe Y. Vardi

Authors
  1. Deian Tabakov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kristin Y. Rozier
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Deian Tabakov.

Additional information

Work supported in part by NSF grants CCF-0613889, CCF-0728882, and Grant EIA-0216467, BSF grant 9800096, the Shared University Grid at Rice (SUG@R), NASA’s Airspace Systems Program, a gift from Intel, and a partnership between Rice University, Sun Microsystems, and Sigma Solutions.

A preliminary version of this work was reported by D. Tabakov and M.Y. Vardi in “Optimized temporal monitors for SystemC,” Proc. 1st Int’l Conf. on Runtime Verification, Lecture Notes in Computer Science 6418, Springer, pp. 436–451, 2010.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Tabakov, D., Rozier, K.Y. & Vardi, M.Y. Optimized temporal monitors for SystemC. Form Methods Syst Des 41, 236–268 (2012). https://doi.org/10.1007/s10703-011-0139-8

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-011-0139-8

Keywords

Search

Navigation