بررسی سیستم های توزیع تطبیق پذیر
ترجمه نشده

بررسی سیستم های توزیع تطبیق پذیر

عنوان فارسی مقاله: یک چارچوب مدولار برای بررسی سیستم های توزیع تطبیق پذیر
عنوان انگلیسی مقاله: A modular framework for verifying versatile distributed systems
مجله/کنفرانس: مجله روشهای منطقی و جبری در برنامه نویسی - Journal of Logical and Algebraic Methods in Programming
رشته های تحصیلی مرتبط: کامپیوتر
گرایش های تحصیلی مرتبط: مهندسی نرم افزار، برنامه نویسی کامپیوتر، معماری سیستم های کامپیوتری
کلمات کلیدی فارسی: سیستم های توزیع شده، سرنام سه حرفی مثبت، ارتباط غیر همزمان، چندپخشی، بررسی سازگاری
کلمات کلیدی انگلیسی: Distributed systems، TLA+، Asynchronous communication، Multicast، Compatibility checking
نوع نگارش مقاله: مقاله پژوهشی (Research Article)
نمایه: Scopus - Master Journals List - JCR
شناسه دیجیتال (DOI): https://doi.org/10.1016/j.jlamp.2019.05.008
دانشگاه: Université de Toulouse, IRIT, 2, rue Charles Camichel, 31000 Toulouse, France
ناشر: الزویر - Elsevier
نوع ارائه مقاله: ژورنال
نوع مقاله: ISI
سال انتشار مقاله: 2019
ایمپکت فاکتور: 1/479 در سال 2018
شاخص H_index: 9 در سال 2019
شاخص SJR: 0/432 در سال 2018
شناسه ISSN: 2352-2208
شاخص Quartile (چارک): Q3 در سال 2018
فرمت مقاله انگلیسی: PDF
تعداد صفحات مقاله انگلیسی: 23
وضعیت ترجمه: ترجمه نشده است
قیمت مقاله انگلیسی: رایگان
آیا این مقاله بیس است: خیر
آیا این مقاله مدل مفهومی دارد: ندارد
آیا این مقاله پرسشنامه دارد: ندارد
آیا این مقاله متغیر دارد: ندارد
کد محصول: E13088
رفرنس: دارای رفرنس در داخل متن و انتهای مقاله
فهرست انگلیسی مطالب

Abstract


1- Context


2- TLA+ specification language


3- Overview of the verification framework


4- Micromodels in detail


5- Properties of multicast and convergecast communication


6- Related work


7- Conclusion


References

نمونه متن انگلیسی مقاله

Abstract


Putting independent components together is a common design practice of distributed systems. Besides, there exists a wide range of interaction protocols that dictate how these components interact, which impacts their compatibility. However, the communication model itself always consists in a monolithic description of the rules and properties of the communication. In this paper, we propose a mechanized framework for the compatibility checking of compositions of peers where the interaction protocol can be fine tuned through assembly of basic properties on the communication. These include whether the communication is point-to-point, multicast or convergecast, which ordering-policies are to be applied, applicative priorities, bounds on the number of messages in transit, and so on. Among these properties, we focus on a generic description of multicast communication that encompasses point-to-point and one-to-all communication as special cases. The components that form the communication model are specified in TLA+, and a system, composed of a communication model and a specification of the behavior of the peers (also in TLA+ ), is checked with the TLA+ model checker. Eventually we provide theoretical views on the relations between ordering-policies through the lenses of multicast and convergecast communication.


Introduction


Distributed systems are a composition of individual components, the peers, that exchange messages and work towards a common goal. Their interactions are governed by a protocol, or communication model, that specifies whether the emission or the reception of a message is possible. For example, synchronous communication dictates that a message shall be sent and received at the same time (rendez-vous). In asynchronous communication, though, which this paper focuses on, the emission and the reception of a message do not happen simultaneously: the two events occur with a delay. This results in many possible interleavings of the communication events, some of which might jeopardize the compatibility or the correction of a composition of peers unless specific properties on the communication are met. Such properties include whether the communication is point-to-point, multicast or convergecast, numerous message-ordering policies that state that some messages have to be delivered in their emission order, bounds on the number of messages in transit, and applicative priorities ensuring that some messages or recipients have precedence over others. Any conjunction of these properties is a unique communication model. Yet, existing verification frameworks consider the interaction protocol to be an indivisible entity that may be, at best, parameterized (e.g. capacity of queues) or entirely substituted by another.

  • اشتراک گذاری در

دیدگاه خود را بنویسید:

تاکنون دیدگاهی برای این نوشته ارسال نشده است

بررسی سیستم های توزیع تطبیق پذیر
نوشته های مرتبط
مقالات جدید
لوگوی رسانه های برخط

logo-samandehi

پیوندها