کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
435134 1441702 2013 19 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols
چکیده انگلیسی

Mutual exclusion protocols are an essential building block of concurrent shared-memory systems: indeed, such a protocol is required whenever a shared resource has to be protected against concurrent non-atomic accesses. Hence, many variants of mutual exclusion protocols exist, such as Peterson’s or Dekker’s well-known protocols. Although the functional correctness of these protocols has been studied extensively, relatively little attention has been paid to their non-functional aspects, such as their performance in the long run. In this paper, we report on experiments with the Cadp toolbox for model checking and performance evaluation of mutual exclusion protocols using Interactive Markov Chains. Steady-state analysis provides an additional criterion for comparing protocols, which complements the verification of their functional properties. We also carefully re-examined the functional properties of these protocols, whose accurate formulation as temporal logic formulas in the action-based setting turns out to be quite involved.


► We illustrate the support for IMCs in CADP.
► We model shared-memory mutual exclusion protocols in LOTOS NT.
► We model check functional properties with EVALUATOR.
► We evaluate the performance with BCG_STEADY and CUNCTATOR.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 78, Issue 7, 1 July 2013, Pages 843–861
نویسندگان
, ,