Integrated Model of Distributed Systems

در سیستم‌های توزیع‌شده مدرن، مانند اینترنت اشیا یا محاسبات ابری، تأیید صحت آنها یک جنبه ضروری است. این امر مستلزم رویکردهای مدل‌سازی است که ویژگی‌های طبیعی چنین سیستم‌هایی را منعکس می‌کند: محلی بودن اجزای آنها، استقلال تصمیمات آنها و ارتباطات ناهمزمان آنها. با این حال، بیشتر تأییدکننده‌های موجود غیرواقعی هستند، زیرا یک یا چند مورد از این ویژگی‌ها منعکس نمی‌شوند. بر این اساس، در این کتاب ما یک فرمالیسم اصلی را ارائه می کنیم: مدل سیستم های توزیع شده یکپارچه (IMDS)، که یک سیستم را به عنوان دو مجموعه (حالت ها و پیام ها) و رابطه ای از "اقدامات" بین این مجموعه ها تعریف می کند. نمای سرور و نمای آژانس مسافرتی از سیستم دوگانگی ارتباطی را ارائه می‌کنند، در حالی که فرمول‌های زمانی عمومی برای IMDS امکان تأیید خودکار را فراهم می‌کنند. ویژگی هایی که مدل بررسی می کند عبارتند از: بن بست جزئی و خاتمه جزئی، بن بست ارتباطی و بن بست منابع. تأیید خودکار می تواند از توسعه سریع سیستم های توزیع شده پشتیبانی کند. علاوه بر این، بر اساس IMDS، ابزار Dedan برای تأیید خودکار سیستم های توزیع شده توسعه یافته است.

In modern distributed systems, such as the Internet of Things or cloud computing, verifying their correctness is an essential aspect. This requires modeling approaches that reflect the natural characteristics of such systems: the locality of their components, autonomy of their decisions, and their asynchronous communication. However, most of the available verifiers are unrealistic because one or more of these features are not reflected. Accordingly, in this book we present an original formalism: the Integrated Distributed Systems Model (IMDS), which defines a system as two sets (states and messages), and a relation of the "actions" between these sets. The server view and the traveling agent’s view of the system provide communication duality, while general temporal formulas for the IMDS allow automatic verification. The features that the model checks include: partial deadlock and partial termination, communication deadlock and resource deadlock. Automatic verification can support the rapid development of distributed systems. Further, on the basis of the IMDS, the Dedan tool for automatic verification of distributed systems has been developed.