Top

Formal Methods in System Design

Published in:

18-07-2017

Introduction to the special issue on runtime verification

Authors: Ezio Bartocci, Rupak Majumdar

Published in: Formal Methods in System Design | Issue 1/2017

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Runtime verification (RV) consists of a broad collection of light-weight scalable analysis techniques to verify and to guarantee at runtime important properties such as correctness, safety, reliability, security, and robustness. The papers in this special issue address some of the RV core problems providing an overview of a wide range of application domains where RV tools and techniques are currently employed. The papers are based on selected contributions from the 2015 Conference on Runtime Verification, an annual forum for scientists from both academia and industry to discuss on how to monitor, analyze and guide the execution of programs and from the 2015 Workshop on Static Analysis meets Runtime Verification.

next article Robust online monitoring of signal temporal logic

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Ahrendt W, Chimento JM, Pace GJ, Schneider G (2017) Verifying data- and control-oriented properties combining static and runtime verification: theory and tools. Formal Methods Syst Des. doi:10.1007/s10703-017-0274-y

Bartocci E, Bortolussi L, Nenzi L (2013) A temporal logic approach to modular design of synthetic biological circuits. In: Proceedings of CMSB 2013: the 11th international conference on computational methods in systems biology, pp 164–177. doi:10.1007/978-3-642-40708-6_13

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. Int J Softw Tools Technol Transf. doi:10.1007/s10009-017-0454-5

Bartocci E, Lió P (2016) Computational modeling, formal analysis, and tools for systems biology. PLoS Comput Biol. doi:10.1371/journal.pcbi.1004591

Bozzelli L, Sánchez C (2016) Foundations of boolean stream runtime verification. Theor Comput Sci 631:118–138. doi:10.1016/j.tcs.2016.04.019 MathSciNetCrossRefMATH

Bufo S, Bartocci E, Sanguinetti G, Borelli M, Lucangelo U, Bortolussi L (2014) Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Steffen B, Margaria T (eds) Proceedings of ISoLA 2014: 6th international symposium on leveraging applications of formal methods, verification and validation, LNCS, vol 8803, pp 391–403. doi:10.1007/978-3-662-45231-8

Cameron F, Fainekos GE, Maahs DM, Sankaranarayanan S (2015) Towards a verified artificial pancreas: challenges and solutions for runtime verification. In: Proceedings of RV 2015: the 6th international conference on runtime verification, LNCS, vol 9333, pp 3–17. Springer. doi:10.1007/978-3-319-23820-3_1

Deshmukh JV, Donzé A, Ghosh S, Jin X, Juniwal G, Seshia SA (2017) Robust online monitoring of signal temporal logic. Formal Methods Syst Des. doi:10.1007/s10703-017-0286-7

Donzé A, Ferrère T, Maler O (2013) Efficient robust monitoring for STL. In: Proceedings of CAV 2013: the 25th international conference on computer aided verification, LNCS, vol 8044, pp 264–279. Springer. doi:10.1007/978-3-642-39799-8_19

10.

Donzé A, Maler O, Bartocci E, Nickovic D, Grosu R, Smolka SA (2012) On temporal logic and signal processing. In: Chakraborty S , Mukund M (eds) Proceedings of ATVA 2012: 10th international symposium on automated technology for verification and analysis, Thiruvananthapuram, October 3–6. Lecture notes in computer science, vol 7561, pp 92–106. Springer. doi:10.1007/978-3-642-33386-6_9

11.

Falcone Y, Havelund K, Reger G (2013) 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. IOS Press, Amsterdam, pp 141–175. doi:10.3233/978-1-61499-207-3-141

12.

Francalanza A, Aceto L, Ingolfsdottir A (2017) Monitorability for the Hennessy-Milner logic with recursion. Formal Methods Syst Des. doi:10.1007/s10703-017-0273-z

13.

Jaksic S, Bartocci E, Grosu R, Kloibhofer R, Nguyen T, Nickovic D (2015) From signal temporal logic to FPGA monitors. In: Proceedings of MEMOCODE 2015: the 13th ACM–IEEE international conference on formal methods and models for system design. ACM, pp 218–227. doi:10.1109/MEMCOD.2015.7340489

14.

Kassem A, Falcone Y, Lafourcade P (2017) Formal analysis and offline monitoring of electronic exams. Formal Methods Syst Des. doi:10.1007/s10703-017-0280-0

15.

Larsen KG (1990) Proof systems for satisfiability in hennessy-milner logic with recursion. Theor Comput Sci 72(2&3):265–288. doi:10.1016/0304-3975(90)90038-J MathSciNetCrossRefMATH

16.

Leucker M, Schallhart C (2009) A brief account of runtime verification. J Log Algebr Program 78(5):293–303. doi:10.1016/j.jlap.2008.08.004 CrossRefMATH

17.

Maler O, Nickovic D (2013) Monitoring properties of analog and mixed-signal circuits. STTT 15(3):247–268. doi:10.1007/s10009-012-0247-9 CrossRef

18.

Moosbrugger PC, Rozier KY, Schumann J (2017) R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. Formal Methods in Syst Des. doi:10.1007/s10703-017-0275-x

19.

Phan D, Yang J, Grosu R, Smolka SA, Stoller SD (2017) Collision avoidance for mobile robots with limited sensing and limited information about moving obstacles. Formal Methods Syst Des. doi:10.1007/s10703-016-0265-4

20.

Pinisetty S, Preoteasa V, Tripakis S, Jéron T, Falcone Y, Marchand H (2017) Predictive runtime enforcement. Formal Methods Syst Des. doi:10.1007/s10703-017-0271-1

21.

Rodionova A, Bartocci E, Nickovic D, Grosu R (2016) Temporal logic as filtering. In: Proceedings of HSCC 2016: the 19th international conference on hybrid systems, pp 11–20. ACM. doi:10.1145/2883817

22.

Sha L (2001) Using simplicity to control complexity. IEEE Softw 18(4):20–28. doi:10.1109/MS.2001.936213 MathSciNetCrossRef

23.

Tuncali CE, Pavlic TP, Fainekos GE (2016) Utilizing S-TaLiRo as an automatic test generation framework for autonomous vehicles. In: Proceedings of ITSC 2016: the 19th IEEE international conference on intelligent transportation, pp 1470–1475. IEEE. doi:10.1109/ITSC.2016.7795751

Title: Introduction to the special issue on runtime verification
Authors: Ezio Bartocci
Rupak Majumdar
Publication date: 18-07-2017
Publisher: Springer US
Published in: Formal Methods in System Design / Issue 1/2017
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-017-0287-6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 1/2017

Formal analysis and offline monitoring of electronic exams

Predictive runtime enforcement

Robust online monitoring of signal temporal logic

Verifying data- and control-oriented properties combining static and runtime verification: theory and tools

Monitorability for the Hennessy–Milner logic with recursion

Collision avoidance for mobile robots with limited sensing and limited information about moving obstacles

Premium Partner