Configuration of Inter-Process Communication with Probabilistic Model Checking

Research output: Contribution to journalResearch articleContributedpeer-review

Abstract

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.

Details

Original languageEnglish
Pages (from-to)651-666
Number of pages16
JournalInternational Journal on Software Tools for Technology Transfer
Volume21
Issue number6
Publication statusPublished - 1 Dec 2019
Peer-reviewedYes

External IDs

Scopus 85074634656
ORCID /0000-0002-5321-9343/work/142236710

Keywords

Keywords

  • configuration, inter-process communication, probabilistic model checking