A brief account of runtime verification

DOI10.1016/j.jlap.2008.08.004zbMath1192.68433MaRDI QIDQ2390027

Martin Leucker, Christian Schallhart

Publication date: 20 July 2009

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2008.08.004

zbMATH Keywords

verification; testing; monitoring; assertion checking

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Foundations of Boolean stream runtime verification, An extended framework for passive asynchronous testing, An approach for lifetime reliability analysis using theorem proving, Deciding safety and liveness in TPTL, Observation strategies for event detection with incidence on runtime verification: theory, algorithms, experimentation, Development of global specification for dynamically adaptive software, Runtime enforcement monitors: Composition, synthesis, and enforcement abilities, Debugging Maude programs via runtime assertion checking and trace slicing, A trace-based model for multiparty contracts, Enforcement and validation (at runtime) of various notions of opacity, A formal approach to adaptive software: continuous assurance of non-functional requirements, Extended Nested Dual System Groups, Revisited, A Theory of Monitors, A Normalized Form for FIFO Protocols Traces, Application to the Replay of Mode-based Protocols

Uses Software

• Coq
• JPAX
• AMT
• LOLA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Safety, liveness and fairness in temporal logic
• An overview of the runtime verification tool Java PathExplorer
• LTL over integer periodicity constraints
• Model-based testing of reactive systems. Advanced lectures.
• A theory of contracts for web services
• From MITL to Timed Automata
• Reasoning about Conditions and Exceptions to Laws in Regulatory Conformance Checking
• Impartial Anticipation in Runtime-Verification
• Run-Time Monitoring of Electronic Contracts
• Comparing LTL Semantics for Runtime Verification
• Safe Runtime Verification of Real-Time Properties
• The complexity of propositional linear temporal logics
• Testing Software Design Modeled by Finite-State Machines
• Monitoring of Real-Time Properties
• Fault Diagnosis for Timed Automata
• A Formal Language for Electronic Contracts
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• An axiomatic basis for computer programming
• Foundations of Software Science and Computational Structures
• Computer Aided Verification
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Model checking of safety properties