Advertisement

Formal Methods in System Design

, Volume 53, Issue 1, pp 1–5 | Cite as

Introduction to the special issue on runtime verification

  • Yliès Falcone
  • César Sánchez
Article
  • 135 Downloads

Abstract

This article introduces the extended versions of selected papers from the refereed proceedings of the 16th International Conference on Runtime Verification (RV 2016) held in Madrid, Spain, in September 2016. Runtime verification encompasses all aspects of monitoring and analysis of hardware, software, and system executions in general. Runtime verification techniques are lightweight dynamic techniques to assess and enforce correctness, reliability, and robustness during system execution. These techniques are significantly more powerful and versatile than conventional testing, and more practical than exhaustive formal verification (at the price of incomplete coverage).

Keywords

Runtime verification Monitoring Reliability Trace Instrumentation 

1 Runtime verification

Runtime verification (RV) is the umbrella term to encompass all aspects of monitoring and analysis of hardware, software and the executions of systems in general. RV techniques are lightweight dynamic techniques to assess and enforce correctness, reliability, and robustness during system execution. These techniques are significantly more powerful, versatile and rigorous than conventional testing, and more practical than exhaustive formal verification. Foundational papers on RV include [1, 2, 3, 4, 5]; see also [6, 7, 8, 9, 10, 11] for tutorial papers. Recently, a tutorial book on RV has been released [12] presenting introductory and advanced topics, including the monitoring of cyber-physical systems [13], runtime failure prevention and reaction [14], monitoring concurrency errors [15], monitoring decentralized and distributed systems [16], and financial and transaction systems [17].

In the last decade, runtime verification, as a computer science field, has grown significantly. As an event, RV—which started initially as a workshop—became a conference in 2010 [18]. Three competitions on software for runtime verification have been organized in so far (see  [19, 20, 21] and [22] for an extensive report of the first incarnation of the competition) as well as a workshop reporting reflections on past competitions [23]. Additionally, two graduate schools (see [24]) devoted to runtime verification have been recently organized in 20161 and 2018.2 A European COST Action on Runtime Verification (IC 1402, runtime verification beyond monitoring3) is ongoing with the objectives of connecting runtime verification to other analysis techniques, and expanding the applicability of RV beyond software reliability. Workshops on particular aspects of runtime verification have also flourished: the AD-RV track [25, 26] at ISoLA 20144 on general applications of runtime verification, the iAD-RV [27] track on industrial applications of runtime verification at ISoLA 2016,5 the PrePost workshop on pre and post deployment technique in 2016, and the recent RUME6 and VORTEX7 workshops on embedded systems and object-oriented languages, respectively.

As the area is getting increasingly mature, deeper results are generated tackling more complex problems. This special issue contains extended versions of selected papers from the RV 2016 conference, as a witness to this maturity.

2 Summaries of the selected articles

In this section, we briefly summarize the articles contained in this special issue. All articles are significantly extend the corresponding papers from the refereed proceedings [28] of the 16th International Conference on Runtime Verification, RV 2016, held in Madrid, Spain, in September 2016.

Goubault-Larrecq and Lachance [29] use monitoring for intrusion detection via their tool Orchids. Their paper addresses the problem of determining the complexity of monitoring an Orchids signature (a specification) and provide a linear-time algorithm that determines whether the number of monitors for this specification is linear or exponential in the number of events.

Shi et al. [30] validate at runtime wireless protocol using wireless sniffers to avoid device instrumentation. They address the problem of losses caused by wireless propagation which prevents the construction of complete traces. Protocols are expressed as a state machine which encodes the uncertainty of sniffers by adding non-determinism. The validation problem is framed as a decision problem, shown to be NP-complete, and they provide an algorithm for exhaustively exploring mutated traces. The algorithm can be enhanced by protocol-oblivious heuristics to select most likely mutated traces.

Kauffman et al. [31] infer abstractions of event streams produced by telemetry systems of the Curiosity rover on Mars. Their approach introduces a hierarchy of event abstractions that can be queried and visualized. Event abstractions are expressed as a rule-based system inspired by Allen’s temporal logic. The approach is implemented in both the C and the Scala programming languages and the specification formalism as both internal and external domain-specific languages.

Jakšić et al. [32] monitor the physical behavior of cyber-physical systems. They provide a quantitative semantics of Signal Temporal Logic by introducing a weighted edit distance. The decision procedure is a dynamic programming algorithm which allows quantifying the similarity between the system and specification behaviors. Hardware-based monitors are implemented on an FPGA, assessed on automotive benchmarks, and used on a magnetic sensor of modern cars.

Moreno and Fischmeister [33] enforce the safety and security of embedded systems using power consumption. Their approach is non-intrusive and consists in analyzing the signal and the system using a spectral analysis that matches the input and output signal. The approach leverages the control-flow graph of the program for performance improvement. They present experiments on a SCADE application and a case study where anomalous executions are detected.

Roşu [34] introduces a sound and complete direct proof system for linear-temporal logic with (only) finite traces. The proof system consists of seven rules extending the proof system of propositional logic, six rules are rather expected, and one special rule is of coinductive nature. Roşu shows that this rule is strictly more powerful than the classical inductive rule used in existing proof systems for infinite and infinite-finite traces.

Footnotes

  1. 1.

    www.rv2016.imag.fr/?page_id=128.

  2. 2.
  3. 3.
  4. 4.
  5. 5.

    isola-conference.org/isola2016/.

  6. 6.

    beru.univ-brest.fr/RUME18.html.

  7. 7.

    conf.researchr.org/track/vortex-2018/vortex-2018-papers.

References

  1. 1.
    Kim M, Viswanathan M, Ben-Abdallah H, Kannan S, Lee I, Sokolsky O (1999) Formally specified monitoring of temporal properties. In: Proceedings of the 11th Euromicro conference on real-time systems (ECRTS 1999), pp 114–122. IEEE Computer SocietyGoogle Scholar
  2. 2.
    Sokolsky O, Kannan S, Kim M, Lee I, Viswanathan M (1999) Steering of real-time systems based on monitoring and checking. In: Proceedings of the Fifth international workshop on object-oriented real-time dependable systems, WORDS’99, pp 11–18. IEEE Computer SocietyGoogle Scholar
  3. 3.
    Havelund K, Rosu G (2001) Monitoring programs using rewriting. In: Proceedings of the 16th IEEE international conference on automated software engineering (ASE 2001), pp 135–143. IEEE Computer SocietyGoogle Scholar
  4. 4.
    Giannakopoulou D, Havelund K (2001) Automata-based verification of temporal properties on running programs. In: Proceedings of the 16th IEEE international conference on automated software engineering (ASE 2001), pp 412–416. IEEE Computer SocietyGoogle Scholar
  5. 5.
    Viswanathan M, Kim M (2004) Foundations for the run-time monitoring of reactive systems—fundamentals of the MaC language. In: Zhiming L, Keijiro A (ed) Revised selected papers from the first international colloquium on theoretical aspects of computing (ICTAC 2004), volume 3407 of LNCS. Springer, Berlin, pp 543–556Google Scholar
  6. 6.
    Havelund K, Goldberg A (2005) Verify your runs. In: Bertrand M, Jim W (eds) Revised selected papers and discussions from the first IFIP TC 2/WG 2.3 conference on verified software: theories, tools, experiments, (VSTTE 2005), volume 4171 of LNCS. Springer, Berlin, pp 374–383Google Scholar
  7. 7.
    Leucker M, Schallhart C (2009) A brief account of runtime verification. J Log Algebr Program 78(5):293–303CrossRefMATHGoogle Scholar
  8. 8.
    Falcone Y (2010) You should better enforce than verify. In: Barringer et al. [18], pp 89–105Google Scholar
  9. 9.
    Falcone Y, Havelund K, Reger G (2013) A tutorial on runtime verification. In: Manfred B, Peled DS, Georg K (eds) Engineering dependable software systems, volume 34 of NATO science for peace and security series, d: information and communication security . IOS Press, pp 141–175Google Scholar
  10. 10.
    Falcone Y, Jean-Claude F, Mounier L (2014) On the expressiveness of some runtime validation techniques. In: Andrei V, Margarita VK (eds) HOWARD-60: a Festschrift on the occasion of Howard Barringer’s 60th birthday, volume 42 of EPiC series in computing. EasyChair, pp 112–123Google Scholar
  11. 11.
    Bartocci E, Falcone Y, Francalanza A, Reger G. (2018) Introduction to runtime verification. In: Bartocci, Falcone [12], pp 1–33Google Scholar
  12. 12.
    Bartocci E, Falcone Y (eds) (2018) Lectures on runtime verification—introductory and advanced topics, volume 10457 of LNCS. SpringerGoogle Scholar
  13. 13.
    Bartocci E, Deshmukh JV, Donzé A, Fainekos GE, Maler O, Dejan N, Sriram S (2018) Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, Falcone [12], pp 135–175Google Scholar
  14. 14.
    Falcone Y, Mariani L, Rollet A, Saha S. (2018) Runtime failure prevention and reaction. In: Bartocci, Falcone [12], pp 103–134Google Scholar
  15. 15.
    Lourenço JM, Fiedor J, Krena B, Vojnar T (2018) Discovering concurrency errors. In: Bartocci, Falcone [12], pp 34–60Google Scholar
  16. 16.
    Francalanza A, Pérez JA, Sánchez C (2018) Runtime verification for decentralised and distributed systems. In: Bartocci, Falcone [12], pp 176–210Google Scholar
  17. 17.
    Colombo C, Pace GJ (2018) Industrial experiences with runtime verification of financial transaction systems: lessons learnt and standing challenges. In: Bartocci, Falcone [12], pp 211–232Google Scholar
  18. 18.
    Barringer H, Falcone Y, Finkbeiner B, Havelund K, Lee I, Pace GJ, Rosu G, Sokolsky O, Tillmann N (eds) (2010) Proceedings of the first international conference on runtime verification (RV 2010), volume 6418 of LNCS. Springer, BerlinGoogle Scholar
  19. 19.
    Bartocci E, Bonakdarpour B, Falcone Y (2014) First international competition on software for runtime verification. In: Borzoo B, Scott AS (eds) Proceedings of the fifth international conference on runtime verification (RV 2014), volume 8734 of LNCS. Springer, Berlin, pp 1–9Google Scholar
  20. 20.
    Falcone Y, Nickovic D, Reger G, Thoma D (2015) Second international competition on runtime verification CRV 2015. In: Ezio B, Rupak M (eds) Proceedings of the 6th international conference on runtime verification (RV 2015), volume 9333 of LNCS. Springer, Berlin, pp 405–422Google Scholar
  21. 21.
    Reger G, Hallé S, Falcone Y (2016) Third international competition on runtime verification—CRV 2016. In: Falcone, Sánchez [28], pp 21–37Google Scholar
  22. 22.
    Bartocci E, Falcone Y, Bonakdarpour B, Colombo C, Decker N, Havelund K, Joshi Y, Klaedtke F, Milewicz R, Reger G, Rosu G, Signoles J, Thoma D, Zalinescu E, Zhang Y (2017) First international competition on runtime verification: rules, benchmarks, tools, and final results of crv 2014. In: International journal on software tools for technology transfer, Apr 2017Google Scholar
  23. 23.
    Reger G (2017) A report of RV-CuBES 2017. In: Giles Reger and Klaus Havelund, editors, RV-CuBES 2017. An International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, September 15, 2017, Seattle, WA, USA, volume 3 of Kalpa Publications in Computing, pp 1–9. EasyChairGoogle Scholar
  24. 24.
    Colombo, Falcone Y (2016) First international summer school on runtime verification—as part of the arvi COST action 1402. In: Falcone, Sánchez [28], pp 17–20Google Scholar
  25. 25.
    Falcone Y, Zuck LD (2012) Runtime verification: The application perspective. In: Tiziana M, Bernhard S (ed) Proceedings of the 5th international symposium on leveraging applications of formal methods, verification and validation technologies for mastering change (ISoLA 2012), Part I, volume 7609 of LNCS. Springer, Berlin, pp 284–291Google Scholar
  26. 26.
    Falcone Y, Zuck LD (2015) Runtime verification: the application perspective. STTT 17(2):121–123CrossRefGoogle Scholar
  27. 27.
    Bartocci E , Falcone Y (2016) Runtime verification and enforcement, the (industrial) application perspective (track introduction). In: Proceedings of the 7th international symposium on leveraging applications of formal methods, verification and validation: discussion, dissemination, applications (ISoLA 2016), Part II, volume 9953 of LNCS, pp 333–338Google Scholar
  28. 28.
    Falcone Y, Sánchez C eds (2016) Proceedings of the 16th international conference on runtime verification (RV 2016), volume 10012 of LNCS. SpringerGoogle Scholar
  29. 29.
    Goubault-Larrecq J, Lachance J-P (2017) On the complexity of monitoring orchids signatures, and recurrence equations. Formal methods in system designGoogle Scholar
  30. 30.
    Shi J, Lahiri SK, Chandra R, Challen G (2017) Wireless protocol validation under uncertainty. Formal methods in system designGoogle Scholar
  31. 31.
    Kauffman S, Havelund K, Joshi R, Fischmeister S (2018) Inferring event stream abstractions. Formal methods in system designGoogle Scholar
  32. 32.
    Jakšić S, Bartocci E, Grosu R, Nguyen R, Ničković D (2018) Quantitative monitoring of STL with edit distance. Formal methods in system designGoogle Scholar
  33. 33.
    Moreno C, Fischmeister S (2017) Non-intrusive runtime monitoring through power consumption to enforce safety and security properties in embedded systems. Formal methods in system designGoogle Scholar
  34. 34.
    Rosu G (2018) Finite-trace linear temporal logic: Coinductive completeness. Formal methods in system designGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Univ. Grenoble Alpes, CNRS, Inria, Laboratoire d’Informatique de GrenobleGrenobleFrance
  2. 2.IMDEA Software InstituteMadridSpain

Personalised recommendations