Skip to main content
SpringerLink
Log in

Runtime Verification and Enforcement, the (Industrial) Application Perspective (Track Introduction)

  • 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

During the last decade, the runtime verification and enforcement (RVE) community has been incredibly prolific in producing many theories, tools and techniques aiming towards the efficient analysis of systems’ executions and guaranteeing their correctness w.r.t. some desired properties. With the major strides made in recent years, much effort is still needed to make RVE attractive and viable methodologies for industrial use. In addition to industry, numerous other domains, such as security, bio-health monitoring, etc., can gain from RVE. The purpose of the “ Runtime Verification and Enforcement: the (industrial) application perspective” track at ISoLA’16 is to bring together RVE experts and potential application domains to try and advance the state-of-the-art on how to make RVE more useable and attractive to industry and other disciplines.

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

References

  1. Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 164–177. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40708-6_13

    Chapter  Google Scholar 

  2. 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 

  3. Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theor. Comput. Sci. 587, 3–25 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of temporal logic properties. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 23–37. Springer, Heidelberg (2014). doi:10.1007/978-3-319-10512-3_3

    Google Scholar 

  5. Bartocci, E., Liò, P.: Computational modeling, formal analysis, and tools for systems biology. PLoS Comput. Biol. 12(1) (2016)

    Google Scholar 

  6. Bonakdarpour, B., Rajsbaum, S., Fraigniaud, P., Travers, C.: Challenges in fault-tolerant distributed runtime verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 363–370. Springer, Cham (2016)

    Google Scholar 

  7. Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., Lucangelo, U., Bortolussi, L.: Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 391–403. Springer, Heidelberg (2014). doi:10.1007/978-3-662-45231-8_30

    Google Scholar 

  8. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). doi:10.1007/BFb0025774

    Chapter  Google Scholar 

  9. Colombo, C., Pace, G., Camilleri, L., Dimech, C.F.R., Grech, J.P., Magro, A., Sammut, A.C., Adami, K.Z.: Runtime verification for stream processing applications. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 400–406. Springer, Cham (2016)

    Google Scholar 

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

    Chapter  Google Scholar 

  11. Falcone, Y., Fernandez, J., Mounier, L.: What can you verify and enforce at runtime? STTT 14(3), 349–382 (2012)

    Article  Google Scholar 

  12. Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D., Kalus, G. (eds.) Engineering Dependable Software Systems, NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 34, pp. 141–175. IOS Press (2013)

    Google Scholar 

  13. Falcone, Y., Jéron, T., Marchand, H., Pinisetty, S.: Runtime enforcement of regular timed properties by suppressing and delaying events. Syst. Control Lett. 123, 2–41 (2016)

    Google Scholar 

  14. Falcone, Y., Marchand, H.: Enforcement and validation (at runtime) of various notions of opacity. Discrete Event Dyn. Syst. 25(4), 531–570 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  15. Falcone, Y., Mounier, L., Fernandez, J., Richier, J.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38(3), 223–262 (2011)

    Article  MATH  Google Scholar 

  16. 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 

  17. Gol, E.A., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction diffusion systems. In: Proceedings of 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, 15–17 December 2014, pp. 108–113. IEEE (2014)

    Google Scholar 

  18. Gordon, P., Pardo, R., Schneider, G.: On the runtime enforcement of evolving privacy policies in online social networks. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 407–412. Springer, Cham (2016)

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  21. Jaksic, S., Bartocci, E., Grosu, R., Ničković, D.: Quantitative monitoring of STL with edit distance. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 201–218. Springer, Heidelberg (2016). doi:10.1007/978-3-319-46982-9_13

    Chapter  Google Scholar 

  22. Joshi, R., Kauffman, S., Havelund, K.: Towards a logic for inferring properties of event streams. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 394–399. Springer, Cham (2016)

    Google Scholar 

  23. Khoury, R., Hallé, S., Waldmann, O.: Execution trace analysis using LTL-FO+. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 356–362. Springer, Cham (2016)

    Google Scholar 

  24. Lenhart, A., Purcell, K., Smith, A., Zickur, K.: Social media & mobile internet use among teens and young adults. Pew Internet & American Life Project (2010)

    Google Scholar 

  25. Leucker, M., Schmitz, M., Tellinghusen, D.A.: Runtime verification for interconnected medical devices. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 380–387. Springer, Cham (2016)

    Google Scholar 

  26. Mariani, L., Pastore, F.: Dynamic analysis of regression problems in industrial systems: challenges and solutions. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 388–393. Springer, Cham (2016)

    Google Scholar 

  27. Nguyen, T., Bartocci, E., Ničković, D., Grosu, R., Jaksic, S., Selyunin, K.: The HARMONIA project: hardware monitoring for automotive systems-of-systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 371–379. Springer, Cham (2016)

    Google Scholar 

  28. Pinisetty, S., Falcone, Y., Jéron, T., Marchand, H., Rollet, A., Nguena-Timo, O.: Runtime enforcement of timed properties revisited. Formal Methods Syst. Des. 45(3), 381–422 (2014)

    Article  MATH  Google Scholar 

  29. Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006). doi:10.1007/11813040_38

    Chapter  Google Scholar 

  30. Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982). doi:10.1007/3-540-11494-7_22

    Chapter  Google Scholar 

  31. Reger, G., Havelund, K.: What is a trace? A runtime verification perspective. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 339–355. Springer, Cham (2016)

    Google Scholar 

  32. Renard, M., Falcone, Y., Rollet, A., Pinisetty, S., Jéron, T., Marchand, H.: Enforcement of (Timed) properties with uncontrollable events. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 542–560. Springer, Heidelberg (2015). doi:10.1007/978-3-319-25150-9_31

    Chapter  Google Scholar 

  33. Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000)

    Article  Google Scholar 

  34. Schneider, G.: On the specification and enforcement of privacy-preserving contractual agreements. In: Steffen, B., Margaria, T. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 413–419. Springer, Cham (2016)

    Google Scholar 

  35. Selyunin, K., Nguyen, T., Bartocci, E., Ničković, D., Grosu, R.: Monitoring of MTL specifications with IBM’s spiking-neuron model. In: Proceedings of DATE 2016: The 19th Design, Automation and Test in Europe Conference and Exhibition, pp. 924–929. IEEE (2016)

    Google Scholar 

Download references

Acknowledgements

The authors acknowledge the support of the ICT COST Action IC1402 Runtime Verification beyond Monitoring (ARVI). Ezio Bartocci acknowledges also the partial support of the Austrian Science Fund (FWF) and the IKT der Zukunft of Austrian FFG project HARMONIA (nr. 845631).

Author information

Authors and Affiliations

  1. Vienna University of Technology, Vienna, Austria

    Ezio Bartocci

  2. Univ. Grenoble Alpes, Inria, LIG, 38000, Grenoble, France

    Ylies Falcone

Authors
  1. Ezio Bartocci
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ylies Falcone
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ezio Bartocci .

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

Bartocci, E., Falcone, Y. (2016). Runtime Verification and Enforcement, the (Industrial) Application Perspective (Track Introduction). 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_24

Download citation

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

  • 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