More Web Proxy on the site http://driver.im/

article

Model-based Runtime Verification Framework

Authors:

Franz RammigAuthors Info & Claims

Electronic Notes in Theoretical Computer Science (ENTCS), Volume 253, Issue 1

Pages 179 - 193

https://doi.org/10.1016/j.entcs.2009.09.035

Published: 01 October 2009 Publication History

Abstract

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 (safety checking). Notice that our runtime verification works at the model level, thus, we do not need to strictly synchronize this runtime verification with the system execution. In fact, we mainly use the runtime information (current states) obtained from the system execution to reduce the state space (of the system model) to be explored. It means that this model-based runtime verification might run before or after the system execution, i.e., switch alternately between a preventive pre-checking mode and a maintaining post-checking mode. In order to make it run ahead of the system execution for as long time as possible, we present two possible strategies so that this runtime verification can selectively reduce the state space (of the system model) to be explored by making the system model enriched with probabilities and additional information derived and learned at the system testing phase.

References

[1]

Arkoudas, K. and M. Rinard, Deductive Runtime Certification, in: Proceedings of the 2004 Workshop on Runtime Verification (RV 2004), Barcelona, Spain, 2004

[2]

Ausiello, G. and Italiano, G.F., On-line algorithms for polynomially solvable satisfiability problems. J. Log. Program. v10. 69-90.

Digital Library

[3]

Barnett, M. and W. Schulte, Spying on components: A runtime verification technique, in: G.T. Leavens, M. Sitaraman and D. Giannakopoulou, editors, Workshop on Specification and Verification of Component-Based Systems, 2001

[4]

Chen, F. and G. Rosu, Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation, in: Proceedings of the 2003 Workshop on Runtime Verification (RV 2003), Boulder, Colorado, USA, 2003

[5]

Clark, E.M., Grumberg Jr., O. and Peled, D.A., Model Checking. 1999. MIT Press.

Digital Library

[6]

Drusinsky, D., The Temporal Rover and the ATG Rover, in: SPIN, 2000, pp. 323--330

Digital Library

[7]

Dwyer, M. B., G. S. Avrunin and J. C. Corbett, Patterns in property specifications for finite-state verification, in: ICSE '99: Proceedings of the 21st international conference on Software engineering (1999), pp. 411--420

Digital Library

[8]

Easwaran, A., Kannan, S. and Sokolsky, O., Steering of discrete event systems: Control theory approach. Electr. Notes Theor. Comput. Sci. v144. 21-39.

Digital Library

[9]

Frank, U., Giese, H., Klein, F., Oberschelp, O., Schmidt, A., Schulz, B., Vöcking, H. and Witting, K., Selbstoptimierende Systeme des Maschinenbaus - Definitionen und Konzepte. 2004. HNI-Verlagsschriftenreihe, 2004.first edition. Bonifatius GmbH, Paderborn, Germany.

[10]

Havelund, K. and G. Rosu, Java PathExplorer --- a runtime verification tool, in: Proceedings 6th International Symposium on Artificial Intelligence, Robotics and Automation in Space (ISAIRAS'01), Montreal, Canada, 2001

[11]

Kent, S., Model driven engineering, in: IFM '02: Proceedings of the Third International Conference on Integrated Formal Methods (2002), pp. 286--298

Digital Library

[12]

Schuppan, V. and Biere, A., Efficient reduction of finite state model checking to reachability analysis. International Journal on Software Tools for Technology Transfer (STTT). v5. 185-204.

Digital Library

[13]

Shukla, S., Rosenkrantz, D.J., Hunt III, H.B. and Stearns, R.E., A HORNSAT Based Approach to the Polynomial Time Decidability of Simulation Relations for Finite State Processes. 1997. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 1997.American Mathematical Society.

[14]

Tasiran, S. and S. Qadeer, Runtime Refinement Checking of Concurrent Data Structures, in: Proceedings of the 2004 Workshop on Runtime Verification (RV 2004), Barcelona, Spain, 2004

[15]

Zhao, Y., Oberthür, S., Kardos, M. and Rammig, F.-J., Model-based runtime verification framework for self-optimizing systems. Electr. Notes Theor. Comput. Sci. v144. 125-145.

Digital Library

[16]

Zhao, Y., S. Oberthür and F. Rammig, Runtime model checking for safety and consistency of self-optimizing mechatronic systems, in: Proceedings of the 7th International Heinz Nixdorf Symposium: Self-optimzing Mechatronic Systems, Paderborn, Germany, 2008

Cited By

Cimatti ATian CTonetta S(2022)Assumption-based Runtime VerificationFormal Methods in System Design10.1007/s10703-023-00416-z60:2(277-324)Online publication date: 1-Apr-2022
https://dl.acm.org/doi/10.1007/s10703-023-00416-z
Cimatti ATian CTonetta S(2019)NuRV: A nuXmv Extension for Runtime VerificationRuntime Verification10.1007/978-3-030-32079-9_23(382-392)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32079-9_23
Cimatti ATian CTonetta S(2019)Assumption-Based Runtime Verification with Partial Observability and ResetsRuntime Verification10.1007/978-3-030-32079-9_10(165-184)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32079-9_10
Show More Cited By

Model-based Runtime Verification Framework

Recommendations

Model-based Runtime Verification Framework for Self-optimizing Systems

This paper describes a novel on-line model checking approach offered as service of a real-time operating system (RTOS). The verification system is intended especially for self-optimizing component-based real-time systems where self-optimization is ...
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools

Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The ...
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Electronic Notes in Theoretical Computer Science (ENTCS)

Electronic Notes in Theoretical Computer Science (ENTCS) Volume 253, Issue 1

October, 2009

188 pages

ISSN:1571-0661

Issue’s Table of Contents

Copyright © Elsevier B.V. © 2009.

Publisher

Elsevier Science Publishers B. V.

Netherlands

Publication History

Published: 01 October 2009

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 27 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cimatti ATian CTonetta S(2022)Assumption-based Runtime VerificationFormal Methods in System Design10.1007/s10703-023-00416-z60:2(277-324)Online publication date: 1-Apr-2022
https://dl.acm.org/doi/10.1007/s10703-023-00416-z
Cimatti ATian CTonetta S(2019)NuRV: A nuXmv Extension for Runtime VerificationRuntime Verification10.1007/978-3-030-32079-9_23(382-392)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32079-9_23
Cimatti ATian CTonetta S(2019)Assumption-Based Runtime Verification with Partial Observability and ResetsRuntime Verification10.1007/978-3-030-32079-9_10(165-184)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32079-9_10
Szvetits MZdun U(2018)Systematic literature review of the objectives, techniques, kinds, and architectures of models at runtimeSoftware and Systems Modeling (SoSyM)10.1007/s10270-013-0394-915:1(31-69)Online publication date: 21-Dec-2018
https://dl.acm.org/doi/10.1007/s10270-013-0394-9
Truscan DAhmad TSiavashi FTuuttila PShukla RSen SShull FBishop J(2015)A practical application of UPPAAL and DTRON for runtime verificationProceedings of the Second International Workshop on Software Engineering Research and Industrial Practice10.5555/2821387.2821397(39-45)Online publication date: 16-May-2015
https://dl.acm.org/doi/10.5555/2821387.2821397

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents