A brief account of runtime verification
From MaRDI portal
Publication:2390027
DOI10.1016/j.jlap.2008.08.004zbMath1192.68433OpenAlexW2101623441MaRDI QIDQ2390027
Christian Schallhart, Martin Leucker
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
Related Items
The delay and window size problems in rule-based stream reasoning ⋮ Foundations of Boolean stream runtime verification ⋮ Semantic Foundations for Deterministic Dataflow and Stream Processing ⋮ Axiomatizing recursion-free, regular monitors ⋮ Gray-box monitoring of hyperproperties with an application to privacy ⋮ A Normalized Form for FIFO Protocols Traces, Application to the Replay of Mode-based Protocols ⋮ Optimal enforcement of (timed) properties with uncontrollable events ⋮ Passive testing with asynchronous communications and timestamps ⋮ An extended framework for passive asynchronous testing ⋮ On the complexity of determinizing monitors ⋮ Monitorable hyperproperties of nonterminating systems ⋮ Monitorability for the Hennessy-Milner logic with recursion ⋮ Formal analysis and offline monitoring of electronic exams ⋮ An approach for lifetime reliability analysis using theorem proving ⋮ Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic ⋮ Runtime enforcement with reordering, healing, and suppression ⋮ Decentralized runtime verification of message sequences in message-based systems ⋮ Sound concurrent traces for online monitoring ⋮ Deciding safety and liveness in TPTL ⋮ Assumption-based runtime verification ⋮ Enforcement and validation (at runtime) of various notions of opacity ⋮ Runtime Verification with Imperfect Information Through Indistinguishability Relations ⋮ Intuitive modelling and formal analysis of collective behaviour in foraging ants ⋮ A formal approach to adaptive software: continuous assurance of non-functional requirements ⋮ Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic ⋮ Shield synthesis ⋮ Symbolic runtime verification for monitoring under uncertainties and assumptions ⋮ Observation strategies for event detection with incidence on runtime verification: theory, algorithms, experimentation ⋮ Runtime enforcement of timed properties using games ⋮ Runtime verification of real-time event streams using the tool HStriver ⋮ Unnamed Item ⋮ Development of global specification for dynamically adaptive software ⋮ Almost Event-Rate Independent Monitoring of Metric Temporal Logic ⋮ A process calculus approach to detection and mitigation of PLC malware ⋮ RiskStructures: a design algebra for risk-aware machines ⋮ ModelPlex: verified runtime validation of verified cyber-physical system models ⋮ Organising LTL monitors over distributed systems with a global clock ⋮ Monitoring networks through multiparty session types ⋮ Parametric runtime verification is NP-complete and coNP-complete ⋮ Runtime verification for dynamic architectures ⋮ Computer says no: verdict explainability for runtime monitors using a local proof system ⋮ A survey of challenges for runtime verification from advanced application domains (beyond software) ⋮ Runtime enforcement monitors: Composition, synthesis, and enforcement abilities ⋮ Unnamed Item ⋮ Introduction to the special issue on runtime verification ⋮ Introduction to the special issue on runtime verification ⋮ Extended Nested Dual System Groups, Revisited ⋮ Property-Based Testing for Spark Streaming ⋮ Determinizing monitors for HML with recursion ⋮ Debugging Maude programs via runtime assertion checking and trace slicing ⋮ A Theory of Monitors ⋮ A theory of monitors ⋮ Unnamed Item ⋮ A trace-based model for multiparty contracts ⋮ Dynamic data structures for timed automata acceptance ⋮ Automated Synthesis: a Distributed Viewpoint ⋮ Monitoring for Silent Actions ⋮ Efficient abstraction algorithms for predicate detection
Uses Software
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
