Advertisement

Configuration of inter-process communication with probabilistic model checking

  • Linda HerrmannEmail author
  • Martin Küttler
  • Tobias Stumpf
  • Christel Baier
  • Hermann Härtig
  • Sascha KlüppelholzEmail author
Foundations for Mastering Change Quantitative Variability Modelling and Analysis
  • 17 Downloads

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.

Keywords

Formal quantitative tradeoff analysis Probabilistic model checking Efficiency Fault tolerance Automatic parameter synthesis Inter-process communication 

Notes

References

  1. 1.
    Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: 1st International Colloquium on Theoretical Aspects of Computing (ICTAC), ser. LNCS vol. 3407, pp. 280–294 (2005) CrossRefGoogle Scholar
  2. 2.
    Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Formal Aspects Comput. 19(1), 93–109 (2007)CrossRefGoogle Scholar
  3. 3.
    Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3–19 (2011)CrossRefGoogle Scholar
  4. 4.
    Hutschenreiter, L., Baier, C., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. In: Proceedings of the 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF), ser. Electronic Proceedings in Theoretical Computer Science, vol. 256, Open Publishing Association, pp. 16–30 (2017)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: CoRR. arXiv:1702.04311 (2017)
  6. 6.
    Kwiatkowska, M. Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: 23rd International Conference on Computer Aided Verification (CAV), ser. Lecture Notes in Computer Science, vol. 6806, pp. 585–591 (2011)CrossRefGoogle Scholar
  7. 7.
    L4/Fiasco.OC microkernel. https://os.inf.tu-dresden.de/fiasco/overview.html (2016)
  8. 8.
    Saha, G.K.: Approaches to software based fault tolerance. Comput. Sci. J. Mold. 13(2), 193–231 (2005)Google Scholar
  9. 9.
    Leuschner, L., Küttler, M., Stumpf, T., Baier, C., Härtig, H., Klüppelholz, S.: Towards automated configuration of systems with non-functional constraints. In: Proceedings of the 16th Workshop on Hot Topics in Operating Systems (HotOS), ACM, pp. 111–117 (2017)Google Scholar
  10. 10.
    16th Workshop on Hot Topics in Operating Systems. http://www.sigops.org/hotos/hotos17/ (2017)
  11. 11.
    Jakosky, B.M., Lin, R.P., Grebowsky, J.M., Luhmann, J.G., Mitchell, D.F., Beutelschies, G., Priser, T., Acuna, M., Andersson, L., Baird, D., Baker, D., Bartlett, R., Benna, M., Bougher, S., Brain, D., Carson, D., Cauffman, S., Chamberlin, P., Chaufray, J.-Y., Cheatom, O., Clarke, J., Connerney, J., Cravens, T., Curtis, D., Delory, G., Demcak, S., DeWolfe, A., Eparvier, F., Ergun, R., Eriksson, A., Espley, J., Fang, X., Folta, D., Fox, J., Gomez- Rosa, C., Habenicht, S., Halekas, J., Holsclaw, G., Houghton, M., Howard, R., Jarosz, M., Jedrich, N., Johnson, M., Kasprzak, W., Kelley, M., King, T., Lankton, M., Larson, D., Leblanc, F., Lefevre, F., Lillis, R., Mahaffy, P., Mazelle, C., McClintock, W., McFadden, J., Mitchell, D.L., Montmessin, F., Morrissey, J., Peterson, W., Possel, W., Sauvaud, J.-A., Schneider, N., Sidney, W., Sparacino, S., Stewart, A.I.F., Tolson, R., Toublanc, D., Waters, C., Woods, T., Yelle, R., Zurek, R.: The mars atmosphere and volatile evolution (maven) mission. Space Sci. Rev. 195(1), 3–48 (2015)CrossRefGoogle Scholar
  12. 12.
  13. 13.
    Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: 8th International Workshop on Reachability Problems (RP), ser. Lecture Notes in Computer Science, vol. 8762, Springer, pp. 125–137 (2014)Google Scholar
  14. 14.
    Češka, M., Dannenberg, F., Paoletti, N., Kwiatkowska, M., Brim, L.: Precise parameter synthesis for stochastic biochemical systems. Acta Inform. 54(6), 589–623 (2017)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Han, T., Katoen, J., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: Proceedings of the 29th IEEE Real-Time Systems Symposium, RTSS 2008, Barcelona, Spain, 30 November–3 December 2008, pp. 173–182 (2008)Google Scholar
  16. 16.
    Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., Gupta, R.: Formal analysis and validation of continuous time Markov chain based system level power management strategies. In: Proceedings of the 7th Annual IEEE International Workshop on High Level Design Validation and Test (HLDVT’02), W. Rosenstiel, Ed., IEEE Computer Society Press, pp. 45–50 (2002)Google Scholar
  17. 17.
    Moreno, G. A., Cámara, J., Garlan, D., Schmerl, B.: Proactive self-adaptation under uncertainty: a probabilistic model checking approach. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ser. ESEC/ FSE 2015, Bergamo, Italy, pp. 1–12. ACM, New York (2015)Google Scholar
  18. 18.
    Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C. R., Smolka, S. A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, Berlin, Heidelberg, pp. 326–340. Springer, Berlin (2011)CrossRefGoogle Scholar
  19. 19.
    Chen, T., Han, T., Kwiatkowska, M., Qu, H.: Efficient probabilistic parameter synthesis for adaptive systems. DCS, Tech. Rep. RR-13-04, p. 13 (2013)Google Scholar
  20. 20.
    Fränzle, M., Gerwinn, S., Kröger, P., Abate, A., Katoen, J.-P.: Multi-objective parameter synthesis in probabilistic hybrid systems. In: Sankaranarayanan, S., Vicario, E. (eds.) Formal Modeling and Analysis of Timed Systems, pp. 93–107. Springer, Cham (2015)CrossRefGoogle Scholar
  21. 21.
    Jovanović, A., Kwiatkowska, M.: Parameter synthesis for probabilistic timed automata using stochastic game abstractions. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) Reachability Problems, pp. 176–189. Springer, Cham (2014)CrossRefGoogle Scholar
  22. 22.
    Long, F., Rinard, M.: Automatic patch generation by learning correct code. SIGPLAN Not. 51(1), 298–312 (2016)CrossRefGoogle Scholar
  23. 23.
    Bokor, P., Kinder, J., Serafini, M., Suri, N.: Efficient model checking of fault-tolerant distributed protocols. In: IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE Compute Society, pp. 73–84 (2011)Google Scholar
  24. 24.
    Gmeiner, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Tutorial on parameterized model checking of fault-tolerant distributed algorithms. In: 14th International on Formal Methods for Executable Software Models School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM), ser. Lecture Notes in Computer Science, vol. 8483, pp. 122–171. Springer, Berlin (2014)Google Scholar
  25. 25.
    Feather, M.S., Fickas, S., Razermera-Mamy, N.: Model-checking for validation of a fault protection system. In: 6th IEEE International Symposium on High-Assurance Systems Engineering (HASE). IEEE Computer Society, pp. 32–41 (2001)Google Scholar
  26. 26.
    Schneider, F., Easterbrook, S. M., Callahan, J. R., Holzmann, G. J.: Validating requirements for fault tolerant systems using model checking. In: 3rd International Conference on Requirements Engineering (ICRE), IEEE Computer Society, pp. 4–13 (1998)Google Scholar
  27. 27.
    John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: 20th International Symposium on Model Checking Software (SPIN), ser. Lecture Notes in Computer Science vol. 7976, pp. 209–226 (2013)CrossRefGoogle Scholar
  28. 28.
    Bernardeschi, C., Fantechi, A., Gnesi, S.: Model checking fault tolerant systems. Softw. Test., Verif. Reliab. 12(4), 251–275 (2002)CrossRefGoogle Scholar
  29. 29.
    Yeung, W.L., Schneider, S.A.: Formal verification of fault-tolerant software design: the CSP approach. Microprocess. Microsyst. 29(5), 197–209 (2005)CrossRefGoogle Scholar
  30. 30.
    Zhang, M., Lungu, A., Sorin, D. J.: Analyzing formal verification and testing efforts of different fault tolerance mechanisms. In: 24th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems (DFT’09), pp. 277–285 (2009)Google Scholar
  31. 31.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  32. 32.
    Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)CrossRefGoogle Scholar
  33. 33.
    Shannon, C.E.: A mathematical theory of communication. Bell Syst. Tech. J. 27, 623–656 (1948)MathSciNetCrossRefGoogle Scholar
  34. 34.
    Amazon Compute Service Level Agreement: https://aws.amazon.com/de/compute/sla/ (2018)
  35. 35.
    Google Cloud Storage Service Level Agreement: https://cloud.google.com/storage/sla (2016)
  36. 36.
    Meurer, A., Smith, C.P., Paprocki, M., Čertík, O., Kirpichev, S.B., Rocklin, M., Kumar, A., Ivanov, S., Moore, J.K., Singh, S., Rathnayake, T., Vig, S., Granger, B.E., Muller, R.P., Bonazzi, F., Gupta, H., Vats, S., Johansson, F., Pedregosa, F., Curry, M.J., Terrel, A.R., Roučka, Š., Saboo, A., Fernando, I., Kulal, S., Cimrman, R., Scopatz, A.: Sympy: Symbolic computing in python. PeerJ Comput. Sci. 3, e103 (2017)CrossRefGoogle Scholar
  37. 37.
    Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)zbMATHGoogle Scholar
  38. 38.
    Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theoret. Comput. Sci. 735, 111–131 (2018)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  • Linda Herrmann
    • 1
    Email author
  • Martin Küttler
    • 1
  • Tobias Stumpf
    • 1
  • Christel Baier
    • 1
  • Hermann Härtig
    • 1
  • Sascha Klüppelholz
    • 1
    Email author
  1. 1.Technische Universität DresdenDresdenGermany

Personalised recommendations