A survey of challenges for runtime verification from advanced application domains (beyond software)
From MaRDI portal
Publication:2008293
DOI10.1007/S10703-019-00337-WzbMATH Open1425.68268arXiv1811.06740OpenAlexW2967277443WikidataQ124212506 ScholiaQ124212506MaRDI QIDQ2008293FDOQ2008293
Julien Signoles, Gerardo Schneider, João M. Lourenço, Ezio Bartocci, Jose Rufino, Christian Colombo, Wolfgang Ahrendt, Srđan Krstić, Gordon J. Pace, Alexander Weiss, Dmitriy Traytel, Yliès Falcone, Domenico Bianculli, Adrian Francalanza, César Sánchez, Dejan Ničković
Publication date: 25 November 2019
Published in: Formal Methods in System Design (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1811.06740
Cites Work
- Monitoring for Silent Actions
- On the Complexity of Temporal-Logic Path Checking
- Verifiable agent interaction in abductive logic programming
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Hybrid Systems: Computation and Control
- HLIO: mixing static and dynamic typing for information-flow control in Haskell
- Control of systems integrating logic, dynamics, and constraints
- Finding repeated elements
- System design of stochastic models using robustness of temporal properties
- The benefits of relaxing punctuality
- Continuous sampling from distributed streams
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Parameter Synthesis for Hybrid Systems with an Application to Simulink Models
- A brief account of runtime verification
- On Temporal Logic and Signal Processing
- Time, clocks, and the ordering of events in a distributed system
- A lattice model of secure information flow
- Deontic interpreted systems
- Multiple facets for dynamic information flow
- Receding Horizon Temporal Logic Planning
- Robustness of temporal logic specifications for continuous-time signals
- Algorithms for distributed functional monitoring
- Reachability analysis of dynamical systems having piecewise-constant derivatives
- Algorithmic analysis of polygonal hybrid systems. I: Reachability
- Low dimensional hybrid systems -- decidable, undecidable, don't know
- Computing reachable states for nonlinear biological models
- Safer asynchronous runtime monitoring using compensations
- Decentralised LTL monitoring
- Regular Linear Temporal Logic
- Timed regular expressions
- A dynamic deontic logic for complex contracts
- Changing legal systems: legal abrogations and annulments in Defeasible Logic
- From Church and Prior to PSL
- Runtime verification of embedded real-time systems
- Failure-aware Runtime Verification of Distributed Systems
- Property testing. Current research and surveys
- Parametric Trace Slicing and Monitoring
- Synopses for massive data: samples, histograms, wavelets, sketches
- Certification of programs for secure information flow
- Parametric linear dynamic logic
- A theory of system behaviour in the presence of node and link failure
- Challenges in the Specification of Full Contracts
- Distributed system contract monitoring
- Monitoring metric first-order temporal properties
- Characterization of temporal property classes
- Scalable offline monitoring of temporal specifications
- Organising LTL monitors over distributed systems with a global clock
- Reactive synthesis from signal temporal logic specifications
- Robust Satisfaction of Temporal Logic over Real-Valued Signals
- Regular Linear Temporal Logic with Past
- Temporal Logic Verification Using Simulation
- Counting large numbers of events in small registers
- On flow-sensitive security types
- S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems
- Formal methods for discrete-time dynamical systems
- Online timed pattern matching using derivatives
- Trace Diagnostics Using Temporal Implicants
- Timed Pattern Matching
- Monitoring of temporal first-order properties with aggregations
- Formal Methods in Computer-Aided Design
- Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
- Synthesising correct concurrent runtime monitors
- Optimal tracking of distributed heavy hitters and quantiles
- SpaTeL
- Robust online monitoring of signal temporal logic
- Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets
- Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation
- A framework for parameterized monitorability
- Quantitative monitoring of STL with edit distance
- Time robustness in MTL and expressivity in hybrid system falsification
- On the complexity of determinizing monitors
- Mining requirements from closed-loop control models
- A theory for observational fault tolerance
- Functional Monitoring without Monotonicity
- Tight bounds for distributed functional monitoring
- Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems
- Measuring with timed patterns
- Temporal Logic as Filtering
- LTL Path Checking Is Efficiently Parallelizable
- A Theory of Monitors
- Runtime verification of temporal properties over out-of-order data streams
- Monitorability for the Hennessy-Milner logic with recursion
- Consistently-detecting monitors
- Optimal proofs for linear temporal logic on lasso words
- A lower bound on the number of opinions needed for fault-tolerant decentralized run-time monitoring
- Timed epistemic knowledge bases for social networks
- Recovery within long-running transactions
- Almost Event-Rate Independent Monitoring of Metric Temporal Logic
- Path Checking for MTL and TPTL over Data Words
- Localizing Faults in Simulink/Stateflow Models with STL
- A Formal Methods Approach to Pattern Recognition and Synthesis in Reaction Diffusion Networks
Cited In (13)
- Linearization, model reduction and reachability in nonlinear ODEs
- Title not available (Why is that?)
- Runtime monitors for Markov decision processes
- Decentralized deadlock-free enforcement of message orderings in message-based systems
- Runtime abstract interpretation for numerical accuracy and robustness
- Computer says no: verdict explainability for runtime monitors using a local proof system
- Uncertainty in runtime verification: a survey
- Runtime enforcement with reordering, healing, and suppression
- Decentralized runtime verification of message sequences in message-based systems
- Gray-box monitoring of hyperproperties with an application to privacy
- Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability
- Runtime Verification: Passing on the Baton
- Online causation monitoring of signal temporal logic
Uses Software
Recommendations
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)
