A survey of challenges for runtime verification from advanced application domains (beyond software)
From MaRDI portal
Publication:2008293
Abstract: Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.
Recommendations
Cites work
- scientific article; zbMATH DE number 5763313 (Why is no real title available?)
- scientific article; zbMATH DE number 53302 (Why is no real title available?)
- scientific article; zbMATH DE number 108549 (Why is no real title available?)
- scientific article; zbMATH DE number 1263213 (Why is no real title available?)
- scientific article; zbMATH DE number 1179121 (Why is no real title available?)
- scientific article; zbMATH DE number 1947405 (Why is no real title available?)
- scientific article; zbMATH DE number 1794363 (Why is no real title available?)
- scientific article; zbMATH DE number 194565 (Why is no real title available?)
- scientific article; zbMATH DE number 795590 (Why is no real title available?)
- scientific article; zbMATH DE number 7471693 (Why is no real title available?)
- scientific article; zbMATH DE number 5263038 (Why is no real title available?)
- A Formal Methods Approach to Pattern Recognition and Synthesis in Reaction Diffusion Networks
- A brief account of runtime verification
- A dynamic deontic logic for complex contracts
- A framework for parameterized monitorability
- A lattice model of secure information flow
- A lower bound on the number of opinions needed for fault-tolerant decentralized run-time monitoring
- A theory for observational fault tolerance
- A theory of monitors (extended abstract)
- A theory of system behaviour in the presence of node and link failure
- Algorithmic analysis of polygonal hybrid systems. I: Reachability
- Algorithms for distributed functional monitoring
- Almost event-rate independent monitoring of metric temporal logic
- Certification of programs for secure information flow
- Challenges in the Specification of Full Contracts
- Changing legal systems: legal abrogations and annulments in Defeasible Logic
- Characterization of temporal property classes
- Computing reachable states for nonlinear biological models
- Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation
- Consistently-detecting monitors
- Continuous sampling from distributed streams
- Control of systems integrating logic, dynamics, and constraints
- Counting large numbers of events in small registers
- Deontic interpreted systems
- Distributed system contract monitoring
- Efficient parallel path checking for linear-time temporal logic with past and bounds
- Failure-aware runtime verification of distributed systems
- Finding repeated elements
- Formal Methods in Computer-Aided Design
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Formal methods for discrete-time dynamical systems
- From Church and Prior to PSL
- Functional Monitoring without Monotonicity
- HLIO: mixing static and dynamic typing for information-flow control in Haskell
- Hybrid Systems: Computation and Control
- LTL Path Checking Is Efficiently Parallelizable
- Localizing Faults in Simulink/Stateflow Models with STL
- Low dimensional hybrid systems -- decidable, undecidable, don't know
- Measuring with timed patterns
- Mining requirements from closed-loop control models
- Monitorability for the Hennessy-Milner logic with recursion
- Monitoring for silent actions
- Monitoring metric first-order temporal properties
- Monitoring of temporal first-order properties with aggregations
- Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems
- Multiple facets for dynamic information flow
- On flow-sensitive security types
- On runtime enforcement via suppressions
- On temporal logic and signal processing
- On the Complexity of Temporal-Logic Path Checking
- On the complexity of determinizing monitors
- Online timed pattern matching using derivatives
- Optimal proofs for linear temporal logic on lasso words
- Optimal tracking of distributed heavy hitters and quantiles
- Organising LTL monitors over distributed systems with a global clock
- Parameter Synthesis for Hybrid Systems with an Application to Simulink Models
- Parametric Trace Slicing and Monitoring
- Parametric linear dynamic logic
- Property testing. Current research and surveys
- Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
- Quantitative monitoring of STL with edit distance
- Reachability analysis of dynamical systems having piecewise-constant derivatives
- Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets
- Reactive synthesis from signal temporal logic specifications
- Receding Horizon Temporal Logic Planning
- Recovery within long-running transactions
- Regular Linear Temporal Logic
- Regular linear temporal logic with past
- Robust online monitoring of signal temporal logic
- Robust satisfaction of temporal logic over real-valued signals
- Robustness of temporal logic specifications for continuous-time signals
- Runtime verification of embedded real-time systems
- Runtime verification of temporal properties over out-of-order data streams
- S-TaLiRo: a tool for temporal logic falsification for hybrid systems
- Safer asynchronous runtime monitoring using compensations
- Scalable offline monitoring of temporal specifications
- Selective monitoring
- SpaTeL: a novel spatial-temporal logic and its applications to networked systems
- Synopses for massive data: samples, histograms, wavelets, sketches
- Synthesising correct concurrent runtime monitors
- System design of stochastic models using robustness of temporal properties
- Temporal Logic Verification Using Simulation
- Temporal logic as filtering
- The benefits of relaxing punctuality
- Tight bounds for distributed functional monitoring
- Time robustness in MTL and expressivity in hybrid system falsification
- Time, clocks, and the ordering of events in a distributed system
- Timed epistemic knowledge bases for social networks
- Timed pattern matching
- Timed regular expressions
- Trace diagnostics using temporal implicants
- Verifiable agent interaction in abductive logic programming: the SCIFF framework
Cited in
(19)- A brief account of runtime verification
- Runtime abstract interpretation for numerical accuracy and robustness
- Runtime enforcement with reordering, healing, and suppression
- Decentralized runtime verification of message sequences in message-based systems
- Linearization, model reduction and reachability in nonlinear ODEs
- Runtime monitors for Markov decision processes
- Uncertainty in runtime verification: a survey
- Runtime Verification: Passing on the Baton
- Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability
- Runtime verification logics. A language design perspective
- Runtime verification past experiences and future projections
- Collaborative runtime verification with tracematches
- Introduction to the special issue on runtime verification
- Introduction to the special issue on runtime verification
- Online causation monitoring of signal temporal logic
- Decentralized deadlock-free enforcement of message orderings in message-based systems
- scientific article; zbMATH DE number 5719320 (Why is no real title available?)
- Gray-box monitoring of hyperproperties with an application to privacy
- Computer says no: verdict explainability for runtime monitors using a local proof system
Describes a project that uses
Uses Software
This page was built for publication: A survey of challenges for runtime verification from advanced application domains (beyond software)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2008293)
