Configuration of Inter-Process Communication with Probabilistic Model Checking

Linda HerrmannLinda Herrmann, Martin KüttlerMartin Küttler, Tobias StumpfTobias Stumpf, Christel BaierChristel Baier, Hermann HärtigHermann Härtig, Sascha KlüppelholzSascha Klüppelholz

DOI Link

Linda Herrmann, Martin Küttler, Tobias Stumpf, Christel Baier, Hermann Härtig, Sascha Klüppelholz
Configuration of Inter-Process Communication with Probabilistic Model Checking
International Journal on Software Tools for Technology Transfer (STTT), 21(6):651--666, 2019

Details
Bibtex

KurzfassungAbstract
Ever-increasing bit flip rates caused by shrinking hardware tiles increase the demand for resilient systems. In particular, safety- and functionality-critical system parts need to be protected. Inter-process communication is one such critical part. Applying fault tolerance techniques often comes with a configuration problem, since real-world systems typically have tunable system parameters. These need to be configured with respect to certain optimality criterion. The paper addresses the parameter synthesis problem for inter-process communication protocols that are affected by bit flips. Tunable parameters are the probability of error detection and the expected time interval between system refresh. We provide a tool that automatically generates a model of bit-flip-prone inter-process communication for a given set of processes and their communication structure. The tool is used to exemplarily generate a model of a space probe. Parametric extensions of probabilistic model checking are applied to obtain rational functions for the availability of the space probe and other characteristics. We find a configuration setting that maximizes availability and investigates side effects for this configuration. The paper also compares exemplarily for the space probe model the most-standard probabilistic model checking methods (value iteration, interval iteration, and exact model checking) with respect to their time consumption and accuracy and reveals complexity concerns arising when evaluating the rational functions.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{HKSBHK2019,
  author  = {Linda Herrmann and Martin K{\"{u}}ttler and Tobias Stumpf and
             Christel Baier and Hermann H{\"{a}}rtig and Sascha
             Kl{\"{u}}ppelholz},
  title   = {Configuration of Inter-Process Communication with Probabilistic
             Model Checking},
  journal = {International Journal on Software Tools for Technology Transfer
             (STTT)},
  volume  = {21},
  number  = {6},
  year    = {2019},
  pages   = {651--666},
  doi     = {10.1007/S10009-019-00536-0}
}