Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Optimized Temporal Monitors for SystemC

  • Conference paper
Runtime Verification (RV 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6418))

Included in the following conference series:

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 on a synthetic workload and identify a configuration that offers the best performance in terms of runtime overhead.

For a longer version of this paper, as well as source code, see http://www.cs.rice.edu/~vardi/papers . Work supported in part by NSF grants CCF-0613889, and CCF-0728882, BSF grant 9800096, and a gift from Intel.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Grotker, T., Liao, S., Martin, G., Swan, S.: System Design with SystemC. Kluwer Academic Publishers, Norwell (2002)

    Google Scholar 

  2. Gupta, A.: Assertion-based verification turns the corner. IEEE Design and Test of Computers 19, 131–132 (2002)

    Google Scholar 

  3. Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, New York (2006)

    Google Scholar 

  4. Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, New York (2005)

    Google Scholar 

  5. Tabakov, D., Vardi, M., Kamhi, G., Singerman, E.: A temporal language for SystemC. In: FMCAD 2008: Proc. Int. Conf. on Formal Methods in Computer-Aided Design, pp. 1–9. IEEE Press, Los Alamitos (2008)

    Google Scholar 

  6. Tabakov, D., Vardi, M.: Monitoring temporal SystemC properties. In: Proc. 8th Int’l Conf. on Formal Methods and Models for Codesign, pp. 123–132. IEEE, Los Alamitos (2010)

    Google Scholar 

  7. Geist, D., Biran, G., Arons, T., Slavkin, M., Nustov, Y., Farkas, M., Holtz, K., Long, A., King, D., Barret, S.: A methodology for the verification of a “system on chip”. In: Proc. 36th Design Automation Conference, DAC 1999, pp. 574–579. ACM, New York (1999)

    Google Scholar 

  8. Abarbanel, Y., Beer, I., Gluhovsky, L., Keidar, S., Wolfsthal, Y.: Focs: Automatic generation of simulation checkers from formal specifications. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 538–542. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  9. Kupferman, O., Vardi, M.: Model checking of safety properties. Formal methods in System Design 19(3), 291–314 (2001)

    Article  MATH  Google Scholar 

  10. Armoni, R., Korchemny, D., Tiemeyer, A., Vardi, M., Zbar, Y.: Deterministic dynamic monitors for linear-time assertions. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol. 4262, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  11. Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. D’Amorim, M., Roşu, G.: Efficient monitoring of ω-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364–378. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Form. Methods Syst. Des. 24(2), 101–127 (2004)

    Article  MATH  Google Scholar 

  14. Geilen, M.: On the construction of monitors for temporal logic properties. Electr. Notes Theor. Comput. Sci. 55(2) (2001)

    Google Scholar 

  15. Giannakopoulou, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: Int. conf. on Automated Software Engineering, Washington, DC, USA, p. 412. IEEE, Los Alamitos (2001)

    Google Scholar 

  16. Boulé, M., Zilic, Z.: Generating Hardware Assertion Checkers. Springer Publishing Company, Incorporated, Heidelberg (2008)

    Book  Google Scholar 

  17. Kupferman, O., Lampert, R.: On the construction of fine automata for safety properties. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 110–124. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  18. Stolz, V., Bodden, E.: Temporal assertions using AspectJ. Electron. Notes Theor. Comput. Sci. 144(4), 109–124 (2006)

    Article  Google Scholar 

  19. Morin-Allory, K., Borrione, D.: Proven correct monitors from PSL specifications. In: DATE 2006: Proc. Conf. on Design, automation and test in Europe, European Design and Automation Association, pp. 1246–1251 (2006)

    Google Scholar 

  20. Pierre, L., Ferro, L.: A tractable and fast method for monitoring SystemC TLM specifications. IEEE Transactions on Computers 57, 1346–1356 (2008)

    Article  MathSciNet  Google Scholar 

  21. Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  22. Duret-Lutz, A., Poitrenaud, D.: SPOT: An extensible model checking library using transition-based generalized Büchi automata. In: Modeling, Analysis, and Simulation of Computer Systems, pp. 76–83 (2004)

    Google Scholar 

  23. Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149–167. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Hopcroft, J., Ullman, J.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)

    MATH  Google Scholar 

  25. Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL. Technical report, The Weizmann Institute of Science (2005)

    Google Scholar 

  26. Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design 1, 275–288 (1992)

    Article  MATH  Google Scholar 

  27. Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 396–411. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  28. Møller, A.: dk.brics.automaton (2004), http://www.brics.dk/automaton/

  29. Bryant, R.: Graph-based algorithms for Boolean-function manipulation. IEEE Trans. on Computers C-35(8) (1986)

    Google Scholar 

  30. de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  31. Cooper, K.D., Torczon, L.: Engineering a Compiler. Morgan Kaufmann, San Francisco (2004)

    MATH  Google Scholar 

  32. Geldenhuys, J., Hansen, H.: Larger automata and less work for LTL model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 53–70. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  33. Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  34. Hoos, H.H.: Computer-aided design of high-performance algorithms. Technical report, University of British Columbia (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Deian Tabakov & Moshe Y. Vardi

Authors
  1. Deian Tabakov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13 9PL, Manchester, UK

    Howard Barringer

  2. INRIA, Rennes - Bretagne Atlantique, France

    Ylies Falcone

  3. Department of Computer Science, Saarland University, 66123, Saarbrücken, Germany

    Bernd Finkbeiner

  4. Jet Propulsion Laboratory, M/S 3041-285, 4800 Oak Grove Drive, 91109, Pasadena, CA, USA

    Klaus Havelund

  5. PRECISE Center, Department of Computer and Information Science, University of Pennsylvania, 19104, Philadelphia, PA, USA

    Insup Lee  & Oleg Sokolsky  & 

  6. Department of Computer Science, University of Malta, MSD 06, Msida, Malta

    Gordon Pace

  7. Department of Computer Science, University of Illinois at Urbana-Champaign, 201 N. Goodwin, 61801, Urbana, IL, USA

    Grigore Roşu

  8. Microsoft Research,, One Microsoft Way, 98052, Redmond, WA, USA

    Nikolai Tillmann

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Tabakov, D., Vardi, M.Y. (2010). Optimized Temporal Monitors for SystemC. In: Barringer, H., et al. Runtime Verification. RV 2010. Lecture Notes in Computer Science, vol 6418. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16612-9_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16612-9_33

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16611-2

  • Online ISBN: 978-3-642-16612-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation