|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
Saarland University (GERMANY),
University of Oxford (UNITED KINGDOM),
and
INRIA Grenoble / CONVECS team (FRANCE)
|
|---|---|
| Method: |
LNT
PRISM modelling language |
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
PRISM Storm |
| Domain: |
Multiprocessor Computers.
|
| Period: |
2024
|
| Size: |
1.6 million states in the CTMC
|
| Description: |
The Erlangen mainframe was a multiprocessor computer for processing
jobs of different priorities while being subject to hardware failures.
The formal modelling and quantitative analysis of the Erlangen
mainframe was proposed in 1994 as a challenging problem by Ulrich
Herzog and Vassilis Merksiotakis (IMMD-7 team, Erlangen University).
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 CTMCs (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.
This case study was revisited three decades later, with the goal of investigating whether the mainframe example can be described using more recent languages than TIPP, and whether the experiments done thirty years ago can be reproduced using modern tools. For this purpose, two novel formal models of the Erlangen mainframe were developed, one in the automata-based language of PRISM, and another one in LNT. Using three different tools, namely PRISM, Storm, and CADP, all numerical experiments were performed and the same figures as in the original publications were successfully reproduced. |
| Conclusions: |
The fact that three different tools (PRISM, Storm, and CADP) developed
independently give identical results on the same model suggest that
these tools could be used in combination to support safety/security
certification of critical systems.
|
| Publications: |
[Garavel-Hermanns-Parker-24]
Hubert Garavel, Holger Hermanns, and David Parker.
"Revisiting a Pioneering Concurrent Stochastic Problem:
The Erlangen Mainframe". Principles of Verification: Cycling the
Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on
the Occasion of His 60th Birthday, Part II, Aachen, Germany.
Lecture Notes in Computer Science vol. 15261, pp. 46-74.
Springer Verlag, November 2024.
Available on-line at: https://hal.inria.fr/hal-02462085/en and also at: https://www.prismmodelchecker.org/papers/jpk-erlangen.pdf |
| Contact: | Hubert Garavel INRIA Centre of University Grenoble Alpes 655, avenue de l'Europe F-38330 Montbonnot Saint Martin FRANCE Email: hubert.garavel@inria.fr |
| Further remarks: | This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page