Configuration of inter-process communication with probabilistic model checking
| Autor: | Christel Baier, Hermann Härtig, Martin Küttler, Linda Herrmann, Sascha Klüppelholz, Tobias Stumpf |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Optimality criterion
Computer science 020207 software engineering Fault tolerance 02 engineering and technology Interval (mathematics) computer.software_genre Inter-process communication Theory of computation 0202 electrical engineering electronic engineering information engineering Markov decision process Communications protocol Algorithm computer Software Information Systems Parametric statistics |
| Zdroj: | International Journal on Software Tools for Technology Transfer. 21:651-666 |
| ISSN: | 1433-2787 1433-2779 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink