1,720,986 research outputs found
Conformal Predictive Monitoring for Multi-modal Scenarios
No full textWe consider the problem of quantitative predictive monitoring (QPM) of stochastic systems, i.e., predicting at runtime the degree of satisfaction of a desired temporal logic property from the current state of the system. Since computational efficiency is key to enable timely intervention against predicted violations, several state-of-the-art QPM approaches rely on fast machine-learning surrogates to provide prediction intervals for the satisfaction values, using conformal inference to offer statistical guarantees. However, these QPM methods suffer when the monitored agent exhibits multi-modal dynamics, whereby certain modes may yield high satisfaction values while others critically violate the property. Existing QPM methods are mode-agnostic and so would yield overly conservative and uninformative intervals that lack meaningful mode-specific satisfaction information. To address this problem, we present GenQPM, a method that leverages deep generative models, specifically score-based diffusion models, to reliably approximate the probabilistic and multi-modal system dynamics without requiring explicit model access. GenQPM employs a mode classifier to partition the predicted trajectories by dynamical mode. For each mode, we then apply conformal inference to produce statistically valid, mode-specific prediction intervals. We demonstrate the effectiveness of GenQPM on a benchmark of agent navigation and autonomous driving tasks, resulting in prediction intervals that are significantly more informative (less conservative) than mode-agnostic baselines.</p
BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees
Full text linkFault trees are a key model in reliability analysis. Classical static fault trees (SFT) can best be analysed using binary decision diagrams (BDD). State-based techniques are favorable for the more expressive dynamic fault trees (DFT). This paper combines the best of both worlds by following Dugan’s approach: dynamic sub-trees are analysed via model checking Markov models and replaced by basic events capturing the obtained failure probabilities. The resulting SFT is then analysed via BDDs. We implemented this approach in the Storm model checker. Extensive experiments (a) compare our pure BDD-based analysis of SFTs to various existing SFT analysis tools, (b) indicate the benefits of our efficient calculations for multiple time points and the assessment of the mean-time-to-failure, and (c) show that our implementation of Dugan’s approach significantly outperforms pure Markovian analysis of DFTs. Our implementation Storm-dft is currently the only tool supporting efficient analysis for both SFTs and DFTs
Probabilistic Hyperproperties with Rewards
No full textProbabilistic hyperproperties describe system properties that are concerned with the probability relation between different system executions. Likewise, it is desirable to relate performance metrics (e.g., energy, execution time, etc.) between multiple runs. This paper introduces the notion of rewards to the temporal logic HyperPCTL by extending the syntax and semantics of the logic to express the accumulated reward relation among different computations. We demonstrate the application of the extended logic in expressing side-channel timing countermeasures, efficiency in probabilistic conformance, path planning in robotics applications, and recovery time in distributed self-stabilizing systems. We also propose a model checking algorithm for verifying Markov Decision Processes against HyperPCTL with rewards and report experimental results
The Prusti Project:Formal Verification for Rust
No full textRust is a modern systems programming language designed to offer both performance and static safety. A key distinguishing feature is a strong type system, which enforces by default that memory is either shared or mutable, but never both. This guarantee is used to prevent common pitfalls such as memory errors and data races. It can also be used to greatly simplify formal verification, as we demonstrated by developing the Prusti verifier, which can verify rich correctness properties of Rust programs with a very modest annotation overhead. In this paper, we provide an overview of the Prusti project. We outline its main design goals, illustrate examples of its use, and discuss important outcomes from the perspectives of a user, a verification expert, and a tool developer.</p
Robust Computation Tree Logic
Full text linkIt is widely accepted that every system should be robust in that ``small''
violations of environment assumptions should lead to ``small'' violations of
system guarantees, but it is less clear how to make this intuition
mathematically precise. While significant efforts have been devoted to
providing notions of robustness for Linear Temporal Logic (LTL), branching-time
logics, such as Computation Tree Logic (CTL) and CTL*, have received less
attention in this regard. To address this shortcoming, we develop ``robust''
extensions of CTL and CTL*, which we name robust CTL (rCTL) and robust CTL*
(rCTL*). Both extensions are syntactically similar to their parent logics but
employ multi-valued semantics to distinguish between ``large'' and ``small''
violations of the specification. We show that the multi-valued semantics of
rCTL make it more expressive than CTL, while rCTL* is as expressive as CTL*.
Moreover, we show that the model checking problem, the satisfiability problem,
and the synthesis problem for rCTL and rCTL* have the same asymptotic
complexity as their non-robust counterparts, implying that robustness can be
added to branching-time logics for free.Comment: Published in the proceedings of NASA Formal Methods (NFM), 202
An Essence of Domain Engineering:A Basis for Trustworthy Aeronautics and Space Software
No full textBefore software can be designed one must have a reasonable grasp of its requirements. Before requirements can be prescribed one must have a reasonable grasp of the domain in which the software is to serve. So we must study, analyse and describe the application domain. We shall argue that domain science & engineering is a necessary prerequisite for requirements engineering, and hence software design. We survey elements of domain science & engineering – and exemplify some elements of domain descriptions. We finally speculate on the relevance of domain engineering in the context of and aeronautics and space.</p
Timed Automata Learning via SMT Solving
No full textAutomata learning is a technique for automatically inferring models of existing systems, that enables formal verification of black-box systems. In this paper we propose a way of learning timed automata, extended final state machines that can measure the progress of time. We make use of SMT solving to learn timed automata consistent with the observations in a set of timed traces, which can be gathered via active testing or passive monitoring. By imposing a set of restrictions to the learnt models, we ensure that our solutions are not overly general. The presented SMT encoding of the problem allows for two ways of incremental solving and different search orders. We present a prototype implementation with results from case studies and randomly generated timed automata of varying size and complexity. We perform an extensive evaluation over six SMT solvers, using different theories and exploration strategies, as well as incremental and non-incremental solving.</p
Verified Probabilistic Policies for Deep Reinforcement Learning
Full text linkDeep reinforcement learning is an increasingly popular technique for
synthesising policies to control an agent's interaction with its environment.
There is also growing interest in formally verifying that such policies are
correct and execute safely. Progress has been made in this area by building on
existing work for verification of deep neural networks and of continuous-state
dynamical systems. In this paper, we tackle the problem of verifying
probabilistic policies for deep reinforcement learning, which are used to, for
example, tackle adversarial environments, break symmetries and manage
trade-offs. We propose an abstraction approach, based on interval Markov
decision processes, that yields probabilistic guarantees on a policy's
execution, and present techniques to build and solve these models using
abstract interpretation, mixed-integer linear programming, entropy-based
refinement and probabilistic model checking. We implement our approach and
illustrate its effectiveness on a selection of reinforcement learning
benchmarks.Comment: NFM 202
Reachability Analysis of Cyber-Physical Systems Using Symbolic-Numeric Techniques
Full text linkIn this thesis, we address the problem of reachability analysis in cyber-physical systems. These are systems engineered by interfacing computational components with the physical world. They provide partially or fully automated safety-critical services in the form of medical devices, autonomous vehicles, avionics and power systems.
We propose techniques to reason about the reachability of such systems, and provide methods for falsifying their safety properties. We model the cyber component as a software program and the physical component as a hybrid dynamical system. Unlike model based analysis, which uses either a purely symbolic or a numerical approach, we argue in favor of using a combination of the two. We justify this by noting that the software program running on a computer is completely specified and has precise semantics. In contrast, the model of the physical system is only an approximation. Hence, we treat the former as a white box, but treat the latter as a black box. Using symbolic methods for the cyber components and numerical methods for hybrid systems, we carefully capture the complex behaviors of software programs and circumvent the difficulty in analyzing complex models developed through first principles. To combine the two techniques, we use a Counterexample Guided Abstraction Refinement (CEGAR) framework. Furthermore, we explore learning techniques like regression and piecewise affine modeling to estimate and represent black box hybrid dynamical systems for the purpose of falsification.
We use prototype implementations to demonstrate the effectiveness of presented ideas. Using non-trivial benchmarks, we compare their performance against the state of the art. We also comment on their applicability and discuss ideas for further improvement
Reachability Analysis of Cyber-Physical Systems Using Symbolic-Numeric Techniques
Full text linkIn this thesis, we address the problem of reachability analysis in cyber-physical systems. These are systems engineered by interfacing computational components with the physical world. They provide partially or fully automated safety-critical services in the form of medical devices, autonomous vehicles, avionics and power systems.
We propose techniques to reason about the reachability of such systems, and provide methods for falsifying their safety properties. We model the cyber component as a software program and the physical component as a hybrid dynamical system. Unlike model based analysis, which uses either a purely symbolic or a numerical approach, we argue in favor of using a combination of the two. We justify this by noting that the software program running on a computer is completely specified and has precise semantics. In contrast, the model of the physical system is only an approximation. Hence, we treat the former as a white box, but treat the latter as a black box. Using symbolic methods for the cyber components and numerical methods for hybrid systems, we carefully capture the complex behaviors of software programs and circumvent the difficulty in analyzing complex models developed through first principles. To combine the two techniques, we use a Counterexample Guided Abstraction Refinement (CEGAR) framework. Furthermore, we explore learning techniques like regression and piecewise affine modeling to estimate and represent black box hybrid dynamical systems for the purpose of falsification.
We use prototype implementations to demonstrate the effectiveness of presented ideas. Using non-trivial benchmarks, we compare their performance against the state of the art. We also comment on their applicability and discuss ideas for further improvement
- …
