Revisiting a Pioneering Concurrent Stochastic Problem: The Erlangen Mainframe

Hubert Garavel, Holger Hermanns, and David Parker

Principles of Verification: Cycling the Probabilistic Landscape (Part II) - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, volume 15261 of Lecture Notes in Computer Science, pages 46-74. Springer, December 2024

Abstract:

The present article is an essay in research reproducibility after thirty years. We retrospectively consider a challenging problem proposed in 1994 by Ulrich Herzog and Vassilis Merksiotakis. This problem was about a multiprocessor computer, the Erlangen mainframe, that processes jobs of different priorities and is subject to hardware failures. Using the stochastic process algebra TIPP, a formal model of this mainframe was specified, which makes intensive use of parallel composition, multiway synchronisation between two or more concurrent processes, and compound transitions combining synchronised actions with rates of Continuous-Time Markov Chains. From this formal model, probabilistic results about availability, performability, and proper dimensioning of the mainframe were obtained using the TIPP software tools, which are no longer maintained. We investigate whether the same experiments can be reproduced today using state-of-the-art model checkers such as CADP, PRISM, and Storm.

29 pages

PDF

PostScript