Probabilistic Network Fault and Performance Analysis
Quantitative Fault Propagation Analysis for Networked Cyber-Physical Systems.
pdf
Linda
Briesemeister, Grit Denker, Daniel Elenius, Ian Mason, Srivatsan
Varadarajan, Devesh Bhatt, Brendan Hall, Gabor Madl, Wilfried SteinerAbstract:
This paper presents an approach to analyzing a model of networked
cyber-physical systems for fault propagation. We present an
implementation of a probabilistic logic model, which allows for
reasoning via symbolic evaluation as well as numeric evaluation to
perform a quantitative fault analysis. Our models are built from a few
building blocks, which can be instantiated as standard or high
integrity; communication paths can be made redundant, and finally, whole
subsystem blocks can be replicated. We assume an underlying networking
infrastructure of TTEthernet, which allows traffic of time-triggered,
rate-constrained, or best-effort modes with different safety features.
We apply our approach to a case study of a brake-by-wire system that
contains communication flows with different traffic modes according to
their criticality.
Compositional Verification of Hybrid Dynamical Systems
Verification and Synthesis Using Real Quantifier Elimination. pdfThomas Sturm, Ashish Tiwari, ISAACS 2011 Abstract: We present the application of real quanti er elimination to formal veri cation and synthesis of continuous and switched dynamical systems. Through a series of case studies, we show how rst-order formulas over the reals arise when formally analyzing models of complex control systems. Existing off -the-shelf quanti er elimination procedures are not successful in eliminating quanti ers from many of our benchmarks.
We therefore automatically combine three established software components: virtual subtitution based quantifi er elimination in Reduce/Redlog, cylindrical algebraic decomposition implemented in Qepcad, and the simpli er Slfq implemented on top of Qepcad. We use this combination to successfully analyze various models of systems including adaptive cruise control in automobiles, adaptive ight control system, and the classical inverted pendulum problem studied in control theory.
Probabilistic Failure Analysis
TBA
Integrated Design Flow and Verification
TBA