Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Revisiting a Pioneering Concurrent Stochastic Problem: The Erlangen Mainframe

  • 章节

  • 发表日期：

    2025年

查看全文
  • Hubert Garavel,
  • Holger Hermanns,
  • David Parker

摘要

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.