کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4952391 | 1364445 | 2016 | 15 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Probabilistic rely-guarantee calculus
ترجمه فارسی عنوان
محاسبه تضمین اعتبار احتمالی
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
برنامه های احتمالی همبستگی، تضمین تضمین تأیید برنامه، معانی برنامه، جبر کلاین ساختارهای رویداد،
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
Jones' rely-guarantee calculus for shared variable concurrency is extended to include probabilistic behaviours. We use an algebraic approach that is based on a combination of probabilistic Kleene algebra with concurrent Kleene algebra. Soundness of the algebra is shown relative to a general probabilistic event structure semantics. The main contribution of this paper is a collection of rely-guarantee rules built on top of that semantics. In particular, we show how to obtain bounds on probabilities of correctness by deriving quantitative extensions of rely-guarantee rules. The use of these rules is illustrated by a detailed verification of a simple probabilistic concurrent program: a faulty Eratosthenes sieve.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 655, Part B, 6 December 2016, Pages 120-134
Journal: Theoretical Computer Science - Volume 655, Part B, 6 December 2016, Pages 120-134
نویسندگان
Annabelle McIver, Tahiry Rabehaja, Georg Struth,