poster

Deciding weak monitorability for runtime verification

Authors:

Zhe Chen,

Yifan Wu,

Ou Wei,

Bin ShengAuthors Info & Claims

ICSE '18: Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings

Pages 163 - 164

https://doi.org/10.1145/3183440.3195077

Published: 27 May 2018 Publication History

Get Access

Abstract

An important problem in runtime verification is monitorability. If a property is not monitorable, then it is meaningless to check it at runtime, as no satisfaction or violation will be reported in finite steps. In this paper, we revisit the classic definition of monitorability, and show that it is too restrictive for practical runtime verification. We propose a weaker but more practical definition of monitorability, say weak monitorability, and show how to decide weak monitorability for runtime verification.

References

[1]

Andreas Bauer. 2010. Monitorability of omega-regular languages. CoRR abs/1006.3638 (2010).

Google Scholar

[2]

Andreas Bauer, Martin Leucker, and Christian Schallhart. 2007. The Good, the Bad, and the Ugly, But How Ugly Is Ugly?. In Proceedings of the 7th International Workshop on Runtime Verification, RV 2007 (Lecture Notes in Computer Science), Vol. 4839. Springer, 126--138.

Digital Library

Google Scholar

[3]

Andreas Bauer, Martin Leucker, and Christian Schallhart. 2011. Runtime Verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM) 20, 4 (2011), 14.

Digital Library

Google Scholar

[4]

Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, and Zhibin Yang. 2016. Parametric Runtime Verification of C Programs. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016) (Lecture Notes in Computer Science), Vol. 9--636. Springer, 299--315.

Digital Library

Google Scholar

[5]

Martin Leucker and Christian Schallhart. 2009. A brief account of runtime verification. Journal of Logic and Algebraic Programming 78, 5 (2009), 293--303.

Crossref

Google Scholar

[6]

Amir Pnueli and Aleksandr Zaks. 2006. PSL Model Checking and Run-Time Verification Via Testers. In Proceedings of the 14th International Symposium on Formal Methods, FM 2006 (Lecture Notes in Computer Science), Vol. 4085. Springer, 573--586.

Digital Library

Google Scholar

Cited By

View all

Ferrando ACardoso R(2024)Towards partial monitoring: Never too early to give inScience of Computer Programming10.1016/j.scico.2024.103220(103220)Online publication date: Oct-2024
https://doi.org/10.1016/j.scico.2024.103220
Ferrando ACardoso R(2021)Towards Partial Monitoring: It is Always too Soon to Give UpElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.348.3348(38-53)Online publication date: 21-Oct-2021
https://doi.org/10.4204/EPTCS.348.3
Aceto LAchilleos AFrancalanza AIngólfsdóttir ALehtinen K(2021)An operational guide to monitorability with applications to regular propertiesSoftware and Systems Modeling (SoSyM)10.1007/s10270-020-00860-z20:2(335-361)Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1007/s10270-020-00860-z
Show More Cited By

Index Terms

Deciding weak monitorability for runtime verification
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging
  2. Software organization and properties
    1. Extra-functional properties
      1. Software reliability
2. Theory of computation
  1. Formal languages and automata theory
    1. Formalisms
  2. Logic
    1. Logic and verification
    2. Modal and temporal logics

Recommendations

Model-based Runtime Verification Framework

Model-based runtime verification is an extension to the state-of-the-art runtime verification, aimed at checking at runtime the system implementation against the system model (consistency checking) and the system model against the system specification (...
Introduction to the special section on runtime verification

Runtime verification is a relatively recent area of research that concentrates on checking system execution against formally specified behavioral properties. Primary research directions in runtime verification include logics for monitoring, online ...
Decentralized Asynchronous Crash-resilient Runtime Verification
Runtime verification is a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronous distributed ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICSE '18: Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings

May 2018

231 pages

ISBN:9781450356633

DOI:10.1145/3183440

Conference Chair:
Michel Chaudron
Chalmers University of Technology, University of Gothenburg, Sweden
,
General Chair:
Ivica Crnkovic
Chalmers University of Technology, University of Gothenburg, Sweden
,
Program Chairs:
Marsha Chechik
University of Toronto, Canada
,
Mark Harman
Facebook and University College London, United Kingdom

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 May 2018

Check for updates

Author Tags

Qualifiers

Poster

Conference

ICSE '18

Sponsor:

SIGSOFT
IEEE-CS

ICSE '18: 40th International Conference on Software Engineering

May 27 - June 3, 2018

Gothenburg, Sweden

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
116
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)4

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ferrando ACardoso R(2024)Towards partial monitoring: Never too early to give inScience of Computer Programming10.1016/j.scico.2024.103220(103220)Online publication date: Oct-2024
https://doi.org/10.1016/j.scico.2024.103220
Ferrando ACardoso R(2021)Towards Partial Monitoring: It is Always too Soon to Give UpElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.348.3348(38-53)Online publication date: 21-Oct-2021
https://doi.org/10.4204/EPTCS.348.3
Aceto LAchilleos AFrancalanza AIngólfsdóttir ALehtinen K(2021)An operational guide to monitorability with applications to regular propertiesSoftware and Systems Modeling (SoSyM)10.1007/s10270-020-00860-z20:2(335-361)Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1007/s10270-020-00860-z
Kauffman SHavelund KFischmeister S(2021)What can we monitor over unreliable channels?International Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-021-00625-z23:4(579-600)Online publication date: 1-Aug-2021
https://dl.acm.org/doi/10.1007/s10009-021-00625-z
Chen ZChen YHierons RWu Y(2020)Four-Valued Monitorability of -Regular LanguagesFormal Methods and Software Engineering10.1007/978-3-030-63406-3_12(198-214)Online publication date: 1-Mar-2020
https://dl.acm.org/doi/10.1007/978-3-030-63406-3_12
Kauffman SHavelund KFischmeister S(2019)Monitorability over Unreliable ChannelsRuntime Verification10.1007/978-3-030-32079-9_15(256-272)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32079-9_15
Aceto LAchilleos AFrancalanza AIngólfsdóttir ALehtinen K(2019)An Operational Guide to MonitorabilitySoftware Engineering and Formal Methods10.1007/978-3-030-30446-1_23(433-453)Online publication date: 18-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-30446-1_23

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Model-based Runtime Verification Framework

Introduction to the special section on runtime verification

Decentralized Asynchronous Crash-resilient Runtime Verification