Probabilistic analysis of self-stabilizing systems: A case study on a mutual exclusion algorithm

Author(s):  
Mehran Alidoost Nia ◽  
Fathiyeh Faghih
Author(s):  
Dang Duy Bui ◽  
Kazuhiro Ogata

AbstractThe mutual exclusion protocol invented by Mellor-Crummey and Scott (called MCS protocol) is used to exemplify that state picture designs based on which the state machine graphical animation (SMGA) tool produces graphical animations should be better visualized. Variants of MCS protocol have been used in Java virtual machines and therefore the 2006 Edsger W. Dijkstra Prize in Distributed Computing went to their paper on MCS protocol. The new state picture design of a state machine formalizing MCS protocol is assessed based on Gestalt principles, more specifically proximity principle and similarity principle. We report on a core part of a formal verification case study in which the new state picture design and the SMGA tool largely contributed to the successful completion of the formal proof that MCS protocol enjoys the mutual exclusion property. The lessons learned acquired through our experiments are summarized as two groups of tips. The first group is some new tips on how to make state picture designs. The second one is some tips on how to conjecture state machine characteristics by using the SMGA tool. We also report on one more case study in which the state picture design has been made for the mutual exclusion protocol invented by Anderson (called Anderson protocol) and some characteristics of the protocol have been discovered based on the tips.


2014 ◽  
Author(s):  
C.J.. J. Segnini ◽  
M.. Rashwan ◽  
M.J.. J. Hernandez ◽  
J. A. Rojas ◽  
M.A.. A. Infante

Abstract This paper presents a methodology for the probabilistic analysis of an infill or step-out opportunity using numerical simulation. Sensitivity and uncertainty analyses for all involved parameters were evaluated through different experimental design techniques. Subsequently, a proxy model was established to reproduce the numerical model performance. Finally, three appropriate solutions were selected from a large population of realizations corresponding to probabilistic percentiles (90%, 50%, and 10% certainty that the specified volume will be recovered). This proposed methodology helped the asset team to evaluate the well candidates more precisely, confidently, and in less time than the current standard methodology. More knowledge about the variables and their effects on overall outcomes was also gained, which helped the team make more-informed decisions. The workflow used the same numerical modeling software, incorporating and facilitating the changes of both static and dynamic properties simultaneously. A case study from Teak field, on the east coast of Trinidad, illustrates the applicability of the methodology and compares its results to those obtained using the standard workflow for the asset. The methodology is one of the latest developments in reservoir simulation, and it has not yet been incorporated into the operator's common practices and procedures for exploitation of the TSP fields.


Sign in / Sign up

Export Citation Format

Share Document