Specification and Verification in Integrated Model of Distributed Systems (IMDS)

Wiktor B. Daszczuk

Abstract

Distributed systems, such as the Internet of Things (IoT) and cloud computing, are becoming popular. This requires modeling that reflects the natural characteristics of such systems: the locality of independent components, the autonomy of their decisions, and asynchronous communication. Automated verification of deadlocks and distributed termination supports rapid development. Existing techniques do not reflect some features of distribution. Most formalisms are synchronous and/or use some kind of global state, both of which are unrealistic. No model supports the communication duality that allows the integration of a remote procedure call and client-server paradigm into a single, uniform model. The majority of model checkers refer to total deadlocks. Usually, they do not distinguish between communication deadlocks from resource deadlocks and deadlocks from distributed termination. Some verification mechanisms check partial deadlocks at the expense of restricting the structure of the system being verified. The paper presents an original formalism for the modeling and verification of distributed systems. The Integrated Model of Distributed Systems (IMDS) defines a distributed system as two sets: states and messages, and the relationship of the “actions” between these sets. Communication duality provides projections on servers and on traveling agents, but the uniform specification of the verified system is preserved. General temporal formulas over IMDS, independent of the structure of the verified system, allow automated verification. These formulas distinguish between deadlocks and distributed termination, and between communication deadlocks and resource deadlocks. Partial deadlocks and partial termination can be checked. The Dedan tool was developed using IMDS formalism.
Author Wiktor B. Daszczuk (FEIT / IN)
Wiktor B. Daszczuk,,
- The Institute of Computer Science
Journal seriesMDPI Computers, ISSN 2073-431X, (0 pkt)
Issue year2018
Vol7
No4
Pages1-26
Publication size in sheets1.25
Keywords in Englishdistributed systems; distributed system modeling; asynchronous modeling; formal methods; model
DOIDOI:10.3390/computers7040065
URL https://www.mdpi.com/2073-431X/7/4/65
projectDevelopment of new algorithms in the areas of software and computer architecture, artificial intelligence and information systems and computer graphics . Project leader: Arabas Jarosław, , Phone: +48 22 234 7432, start date 01-08-2018, planned end date 30-09-2019, II/2018/DS/1, Implemented
WEiTI Działalność statutowa
Languageen angielski
File
IMDS11[12665].pdf 1.41 MB
Score (nominal)5
ScoreMinisterial score = 5.0, 10-07-2019, ArticleFromJournal
Publication indicators WoS Citations = 0; Scopus Citations = 2
Citation count*1 (2019-08-19)
Cite
Share Share

Get link to the record


* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.
Back