Integrated Model of Distributed Systems
暫譯: 分散式系統的整合模型
Daszczuk, Wiktor B.
- 出版商: Springer
- 出版日期: 2019-03-26
- 售價: $4,480
- 貴賓價: 9.5 折 $4,256
- 語言: 英文
- 頁數: 238
- 裝訂: Hardcover - also called cloth, retail trade, or trade
- ISBN: 3030128342
- ISBN-13: 9783030128340
海外代購書籍(需單獨結帳)
相關主題
商品描述
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.
商品描述(中文翻譯)
在現代分散式系統中,例如物聯網或雲端計算,驗證其正確性是一個重要的方面。這需要建模方法來反映這些系統的自然特性:其組件的區域性、決策的自主性以及非同步通信。然而,大多數可用的驗證器並不現實,因為這些特性中的一個或多個未被反映。因此,在本書中,我們提出了一種原創的形式化方法:整合分散式系統模型(Integrated Distributed Systems Model,IMDS),該模型將系統定義為兩個集合(狀態和消息)以及這些集合之間的“行為”關係。伺服器視圖和旅行代理的系統視圖提供了通信的雙重性,而IMDS的一般時間公式則允許自動驗證。該模型檢查的特性包括:部分死鎖和部分終止、通信死鎖和資源死鎖。自動驗證可以支持分散式系統的快速開發。此外,基於IMDS,已開發出用於分散式系統自動驗證的Dedan工具。