Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

What Is a Trace? A Runtime Verification Perspective

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications (ISoLA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9953))

Included in the following conference series:

Abstract

Runtime Monitoring or Verification deals with traces. In its most simple form a monitoring system takes a trace produced by a system and a specification of correct behaviour and checks if the trace conforms to the specification. More complex applications may introduce notions of feedback and reaction. The notion that unifies the field is that we can abstract the runtime behaviour of a system by an execution trace and check this for conformance. However, there is little uniform understanding of what a trace is. This is most keenly seen when comparing theoretical and practical work. This paper surveys the different notions of trace and reflects on the related issues.

G. Reger—The contribution of this author is based upon work from COST Action ARVI IC1402, supported by COST (European Cooperation in Science and Technology).

K. Havelund—The research performed by this author was carried out at Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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 EPUB and 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

Similar content being viewed by others

Notes

  1. 1.

    http://www.cs.um.edu.mt/svrg/Tools/detectEr.

  2. 2.

    https://www.w3.org/Daemon/User/Config/Logging.html#common-logfile-format.

  3. 3.

    https://www.w3.org/TR/WD-logfile.html.

  4. 4.

    This information is based on that found in man strace.

  5. 5.

    The issue here is that over the lifetime of a program the same memory address could refer to different data structures if some structures are deleted.

  6. 6.

    See http://www.ietf.org/rfc/rfc4180.txt.

  7. 7.

    See https://www.w3.org/TR/REC-xml.

  8. 8.

    See https://tools.ietf.org/html/rfc7159.

References

  1. Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. SIGPLAN Not. 40, 345–364 (2005)

    Article  MATH  Google Scholar 

  2. Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990). doi:10.1007/BFb0032042

    Chapter  Google Scholar 

  3. Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–203 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  4. Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  5. AspectC++. Aspect oriented programming for C++ (2016). http://www.aspectc.org

  6. AspectJ. Aspect oriented programming for Java (2016). https://eclipse.org/aspectj/

  7. Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68–84. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32759-9_9

    Chapter  Google Scholar 

  8. Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: VMCAI, pp. 44–57 (2004)

    Google Scholar 

  9. Barringer, H., Havelund, K.: TraceContract: a scala DSL for trace analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 57–72. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21437-0_7

    Chapter  Google Scholar 

  10. Bartocci, E., Bonakdarpour, B., Falcone, Y.: First international competition on software for runtime verification. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 1–9. Springer, Heidelberg (2014). doi:10.1007/978-3-319-11164-3_1

    Google Scholar 

  11. Bartocci, E., Bonakdarpour, B., Falcone, Y., Colombo, C., Decker, N., Klaedtke, F., Havelund, K., Joshi, Y., Milewicz, R., Reger, G., Rosu, G., Signoles, J., Thoma, D., Zalinescu, E., Zhang, Y.: First international competition on runtime verification. Int. J. Softw. Tools Technol. Transf. (STTT) (to appear, 2016)

    Google Scholar 

  12. Bartocci, E., Bortolussi, L., Milios, D., Nenzi, L., Sanguinetti, G.: Studying emergent behaviours in morphogenesis using signal spatio-temporal logic. In: Abate, A., Šafránek, D. (eds.) HSB 2015. LNCS, vol. 9271, pp. 156–172. Springer, Heidelberg (2015). doi:10.1007/978-3-319-26916-0_9

    Chapter  Google Scholar 

  13. Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 168–182. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35632-2_18

    Chapter  Google Scholar 

  14. Basin, D., Harvan, M., Klaedtke, F., Zălinescu, E.: Monpoly: monitoring usage-control policies. In: Khurshid, S., Sen, K. (eds.) RV 2012. LNCS, vol. 7186, pp. 360–364. Springer, Berlin Heidelberg (2012)

    Chapter  Google Scholar 

  15. Basin, D., Klaedtke, F., Marinovic, S., Zălinescu, E.: Monitoring of temporal first-order properties with aggregations. Formal Methods Syst. Des. 46(3), 262–285 (2015)

    Article  MATH  Google Scholar 

  16. Basin, D., Klaedtke, F., Müller, S., Zălinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1–15:45 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  17. Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27755-2_3

    Chapter  Google Scholar 

  18. Cassar, I., Francalanza, A.: On synchronous and asynchronous monitor instrumentation for actor-based systems. In: Proceedings of the 13th International Workshop on Foundations of Coordination Languages and Self-Adaptive Systems, FOCLASA 2014, Rome, Italy, 6th September 2014, pp. 54–68, 2014 (2014)

    Google Scholar 

  19. Cassar, I., Francalanza, A.: On implementing a monitor-oriented programming framework for actor systems. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 176–192. Springer, Heidelberg (2016). doi:10.1007/978-3-319-33693-0_12

    Chapter  Google Scholar 

  20. Chen, F., Roşu, G.: Parametric trace slicing and monitoring. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 246–261. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00768-2_23

    Chapter  Google Scholar 

  21. Chen, Z., Wang, Z., Zhu, Y., Xi, H., Yang, Z.: Parametric runtime verification of C programs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 299–315. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_17

    Chapter  Google Scholar 

  22. CIL. C Intermediate Language (2016). https://www.cs.berkeley.edu/~necula/cil/

  23. Colombo, C., Francalanza, A., Gatt, R.: Elarva: a monitoring tool for Erlang. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 370–374. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29860-8_29

    Chapter  Google Scholar 

  24. Decker, N., Leucker, M., Thoma, D.: jUnitRV–adding runtime verification to jUnit. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 459–464. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38088-4_34

    Chapter  Google Scholar 

  25. Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 341–356. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_23

    Chapter  Google Scholar 

  26. Demri, S., Lazić, R.: LTL with the freeze quantifier, register automata. ACM Trans. Comput. Logic 10(3), 1–30 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  27. Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 92–106. Springer, Heidelberg (2012)

    Google Scholar 

  28. Dou, W., Bianculli, D., Briand, L.: OCLR: a more expressive, pattern-based temporal extension of OCL. In: Cabot, J., Rubin, J. (eds.) ECMFA 2014. LNCS, vol. 8569, pp. 51–66. Springer, Heidelberg (2014). doi:10.1007/978-3-319-09195-2_4

    Google Scholar 

  29. Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D. (eds.) Summer School Marktoberdorf 2012 - Engineering Dependable Software Systems. IOS Press (2013). to appear

    Google Scholar 

  30. Falcone, Y., Ničković, D., Reger, G., Thoma, D.: Second international competition on runtime verification. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 405–422. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_27

    Chapter  Google Scholar 

  31. Gol, E.A., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction diffusion systems. In: 53rd IEEE Conference on Decision and Control, pp. 108–113, December 2014

    Google Scholar 

  32. Grigore, R., Distefano, D., Petersen, R.L., Tzevelekos, N.: Runtime verification based on register automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 260–276. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_19

    Chapter  Google Scholar 

  33. Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97–105 (2009)

    Article  MATH  Google Scholar 

  34. Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Gros, R., Belta, C.: Spatel: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, pp. 189–198. ACM, New York (2015)

    Google Scholar 

  35. Halle, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5(2), 192–206 (2012)

    Article  MathSciNet  Google Scholar 

  36. Havelund, K.: Runtime verification of C programs. In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds.) FATES/TestCom 2008. LNCS, vol. 5047, pp. 7–22. Springer, Heidelberg (2008). doi:10.1007/978-3-540-68524-1_3

    Chapter  Google Scholar 

  37. Holzmann, G.: Spin Model Checker, The: Primer and Reference Manual, 1st edn. Addison-Wesley Professional (2003)

    Google Scholar 

  38. Huang, J., Meredith, P.O., Rosu, G.: Maximal sound predictive race detection with control flow abstraction. SIGPLAN Not. 49(6), 337–348 (2014)

    Article  Google Scholar 

  39. Jakšić, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Ničkovié, D.: From signal temporal logic to FPGA monitors. In: 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 218–227, September 2015

    Google Scholar 

  40. Kalajdzic, K., Bartocci, E., Smolka, S.A., Stoller, S.D., Grosu, R.: Runtime verification with particle filtering. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 149–166. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40787-1_9

    Chapter  Google Scholar 

  41. Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329–363 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  42. Kim, M.Z., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance approach for java programs. Formal Methods Syst. Des. 24(2), 129–155 (2004)

    Article  MATH  Google Scholar 

  43. Kosmatov, N., Petiot, G., Signoles, J.: An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 167–182. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40787-1_10

    Chapter  Google Scholar 

  44. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)

    Article  Google Scholar 

  45. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic, Algebr. Program. 78(5), 293–303 (2008)

    Article  MATH  Google Scholar 

  46. Lu, H., Forin, A.: The design and implementation of P2V, an architecture for zero-overhead online verification of software programs. Technical Report MSR-TR-2007-99, Microsoft Research, August 2007

    Google Scholar 

  47. Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P.O.N., Şerbănuţă, T.F., Roşu, G.: RV-Monitor: efficient parametric runtime verification with simultaneous properties. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 285–300. Springer, Heidelberg (2014). doi:10.1007/978-3-319-11164-3_24

    Google Scholar 

  48. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30206-3_12

    Chapter  Google Scholar 

  49. Meredith, P., Jin, D., Griffith, D., Chen, F., Roşu, G.: An overview of the MOP runtime verification framework. J. Softw. Tools Technol. Transf., 1–41 (2011)

    Google Scholar 

  50. Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: 2015 IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 494–503, May 2015

    Google Scholar 

  51. Navabpour, S., Joshi, Y., Wu, C.W.W., Berkovich, S., Medhat, R., Bonakdarpour, B., Fischmeister, S.: RiTHM: a tool for enabling time-triggered runtime verification for c programs. In: ACM Symposium on the Foundations of Software Engineering (FSE), pp. 603–606 (2013)

    Google Scholar 

  52. Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic 5(3), 403–435 (2004)

    Article  MathSciNet  Google Scholar 

  53. Ogale, V.A., Garg, V.K.: Detecting temporal logic predicates on distributed computations. In: Pelc, A. (ed.) DISC 2007. LNCS, vol. 4731, pp. 420–434. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75142-7_32

    Chapter  Google Scholar 

  54. Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1–13. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85778-5_1

    Chapter  Google Scholar 

  55. Pastore, F., Mariani, L.: AVA: supporting debugging with failure interpretations. In: Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, 18–22 March 2013, pp. 416–421 (2013)

    Google Scholar 

  56. Pellizzoni, R., Meredith, P., Caccamo, M., Rosu, G.: Hardware runtime monitoring for dependable COTS-based real-time embedded systems. In: Real-Time Systems Symposium 2008, pp. 481–491, November 2008

    Google Scholar 

  57. Reger, G.: Suggesting edits to explain failing traces. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 287–293. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_20

    Chapter  Google Scholar 

  58. Reger, G., Rydeheard, D.: From first-order temporal logic to parametric trace slicing. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 216–232. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_14

    Chapter  Google Scholar 

  59. Renberg, A.: Test-inspired runtime verification. Master’s thesis, Royal Institute of Technology (KTH), Stockholm (2014)

    Google Scholar 

  60. Russ, A.: Detecting security incidents using windows workstation event logs. Technical report, Sans Institute InfoSec Reading Room (2013)

    Google Scholar 

  61. Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41–57. Springer, Heidelberg (2006). doi:10.1007/11874683_3

    Chapter  Google Scholar 

  62. Selyunin, K., Nguyen, T., Bartocci, E., Nickovic, D., Grosu, R.: Monitoring of MTL specifications with IBM’s spiking-neuron model. In: 2016 Design, Automation Test in Europe Conference Exhibition (DATE), pp. 924–929, March 2016

    Google Scholar 

  63. Sen, A., Garg, V.K.: Rv ’2003, run-time verification (satellite workshop of cav ’03) partial order trace analyzer (pota) for distributed programs. Electron. Not. Theoret. Comput. Sci. 89(2), 22–43 (2003)

    Article  Google Scholar 

  64. Sen, A., Garg, V.K.: Detecting temporal logic predicates in distributed programs using computation slicing. In: Papatriantafilou, M., Hunel, P. (eds.) OPODIS 2003. LNCS, vol. 3144, pp. 171–183. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27860-3_17

    Chapter  Google Scholar 

  65. Şerbănuţă, T.F., Chen, F., Roşu, G.: Maximal causal models for sequentially consistent systems. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 136–150. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35632-2_16

    Chapter  Google Scholar 

  66. Seyster, J., Dixit, K., Huang, X., Grosu, R., Havelund, K., Smolka, S.A., Stoller, S.D., Zadok, E.: Interaspect: aspect-oriented instrumentation with GCC. Formal Methods Syst. Des. 41(3), 295–320 (2012)

    Article  MATH  Google Scholar 

  67. Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 193–207. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29860-8_15

    Chapter  Google Scholar 

  68. Stolz, V.: Temporal assertions with parametrized propositions*. J. Log. Comput. 20, 743–757 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  69. Todman, T., Stilkerich, S., Luk, W.: In-circuit temporal monitors for runtime verification of reconfigurable designs. In: Proceedings of the 52nd Annual Design Automation Conference, DAC 2015, pp. 50:1–50:6. ACM, New York (2015)

    Google Scholar 

  70. Watterson, C., Heffernan, D.: Runtime verification and monitoring of embedded systems. IET Softw. 1(5), 172–179 (2007)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Manchester, Manchester, UK

    Giles Reger

  2. Jet Propulsion Laboratory, California Institute of Technology, Pasadena, USA

    Klaus Havelund

Authors
  1. Giles Reger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Klaus Havelund
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Giles Reger .

Editor information

Editors and Affiliations

  1. Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Reger, G., Havelund, K. (2016). What Is a Trace? A Runtime Verification Perspective. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. ISoLA 2016. Lecture Notes in Computer Science(), vol 9953. Springer, Cham. https://doi.org/10.1007/978-3-319-47169-3_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47169-3_25

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47168-6

  • Online ISBN: 978-3-319-47169-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation