A survey of challenges for runtime verification from advanced application domains (beyond software)
From MaRDI portal
Publication:2008293
DOI10.1007/s10703-019-00337-wzbMath1425.68268arXiv1811.06740OpenAlexW2967277443WikidataQ124212506 ScholiaQ124212506MaRDI QIDQ2008293
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)
Full work available at URL: https://arxiv.org/abs/1811.06740
Related Items (8)
Runtime monitors for Markov decision processes ⋮ Gray-box monitoring of hyperproperties with an application to privacy ⋮ 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 ⋮ Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability ⋮ Runtime abstract interpretation for numerical accuracy and robustness ⋮ Computer says no: verdict explainability for runtime monitors using a local proof system
Uses Software
Cites Work
- Formal Methods in Computer-Aided Design
- Timed Pattern Matching
- Hybrid Systems: Computation and Control
- Optimal proofs for linear temporal logic on lasso words
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Decentralised LTL monitoring
- Low dimensional hybrid systems -- decidable, undecidable, don't know
- A dynamic deontic logic for complex contracts
- Runtime verification of embedded real-time systems
- Parametric linear dynamic logic
- Computing reachable states for nonlinear biological models
- Scalable offline monitoring of temporal specifications
- Organising LTL monitors over distributed systems with a global clock
- Property testing. Current research and surveys
- Robustness of temporal logic specifications for continuous-time signals
- Synthesising correct concurrent runtime monitors
- Monitoring of temporal first-order properties with aggregations
- A theory of system behaviour in the presence of node and link failure
- Finding repeated elements
- Control of systems integrating logic, dynamics, and constraints
- Reachability analysis of dynamical systems having piecewise-constant derivatives
- Deontic interpreted systems
- A framework for parameterized monitorability
- Quantitative monitoring of STL with edit distance
- Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation
- Measuring with timed patterns
- Time robustness in MTL and expressivity in hybrid system falsification
- Optimal tracking of distributed heavy hitters and quantiles
- Formal methods for discrete-time dynamical systems
- Timed epistemic knowledge bases for social networks
- Runtime verification of temporal properties over out-of-order data streams
- Online timed pattern matching using derivatives
- A lower bound on the number of opinions needed for fault-tolerant decentralized run-time monitoring
- System design of stochastic models using robustness of temporal properties
- Algorithmic analysis of polygonal hybrid systems. I: Reachability
- A brief account of runtime verification
- On the complexity of determinizing monitors
- Robust online monitoring of signal temporal logic
- Monitorability for the Hennessy-Milner logic with recursion
- Distributed system contract monitoring
- Safer asynchronous runtime monitoring using compensations
- A theory for observational fault tolerance
- Monitoring Metric First-Order Temporal Properties
- A Theory of Monitors
- Recovery within long-running transactions
- Synopses for Massive Data: Samples, Histograms, Wavelets, Sketches
- Multiple facets for dynamic information flow
- HLIO: mixing static and dynamic typing for information-flow control in Haskell
- Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems
- Mining requirements from closed-loop control models
- Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets
- SpaTeL
- Reactive synthesis from signal temporal logic specifications
- Temporal Logic as Filtering
- S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems
- Algorithms for distributed functional monitoring
- Timed regular expressions
- Almost Event-Rate Independent Monitoring of Metric Temporal Logic
- Path Checking for MTL and TPTL over Data Words
- Trace Diagnostics Using Temporal Implicants
- Temporal Logic Verification Using Simulation
- From Church and Prior to PSL
- Regular Linear Temporal Logic
- Changing legal systems: legal abrogations and annulments in Defeasible Logic
- Robust Satisfaction of Temporal Logic over Real-Valued Signals
- Challenges in the Specification of Full Contracts
- Parametric Trace Slicing and Monitoring
- Parameter Synthesis for Hybrid Systems with an Application to Simulink Models
- Functional Monitoring without Monotonicity
- LTL Path Checking Is Efficiently Parallelizable
- Regular Linear Temporal Logic with Past
- A lattice model of secure information flow
- Certification of programs for secure information flow
- Time, clocks, and the ordering of events in a distributed system
- Counting large numbers of events in small registers
- The benefits of relaxing punctuality
- Localizing Faults in Simulink/Stateflow Models with STL
- A Formal Methods Approach to Pattern Recognition and Synthesis in Reaction Diffusion Networks
- On Temporal Logic and Signal Processing
- Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
- Consistently-detecting monitors
- Monitoring for Silent Actions
- On the Complexity of Temporal-Logic Path Checking
- Characterization of temporal property classes
- Failure-aware Runtime Verification of Distributed Systems
- Verifiable agent interaction in abductive logic programming
- On flow-sensitive security types
- Receding Horizon Temporal Logic Planning
- Continuous sampling from distributed streams
- Tight bounds for distributed functional monitoring
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
This page was built for publication: A survey of challenges for runtime verification from advanced application domains (beyond software)
