2020/04/14 by Clemens Dubslaff, Dubslaff, Clemens, Andrey Morozov +5
Computer Science · Decision Sciences · Engineering · #Software Reliability and Analysis Research #Risk and Safety Analysis #Safety Systems Engineering in Autonomy
paper · pdf · doi:10.48550/arxiv.2004.06637
Modern safety-critical systems are heterogeneous, complex, and highly\ndynamic. They require reliability evaluation methods that go beyond the\nclassical static methods such as fault trees, event trees, or reliability block\ndiagrams. Promising dynamic reliability analysis methods employ probabilistic\nmodel checking on various probabilistic state-based models. However, such\nmethods have to tackle the well-known state-space explosion problem. To compete\nwith this problem, reduction methods such as symmetry reduction and\npartial-order reduction have been successfully applied to probabilistic models\nby means of discrete Markov chains or Markov decision processes. Such models\nare usually specified using probabilistic programs provided in guarded command\nlanguage. In this paper, we propose two automated reduction methods for\nprobabilistic programs that operate on a purely syntactic level: reset value\noptimization and register allocation optimization. The presented techniques\nrely on concepts well known from compiler construction such as live range\nanalysis and register allocation through interference graph coloring. Applied\non a redundancy system model for an aircraft velocity control loop modeled in\nSIMULINK, we show effectiveness of our implementation of the reduction methods.\nWe demonstrate that model-size reductions in three orders of magnitude are\npossible and show that we can achieve significant speedups for a reliability\nanalysis.\n