Specification and Verification in Integrated Model of Distributed Systems (IMDS)
Wiktor B. Daszczuk
AbstractDistributed 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.
|Journal series||MDPI Computers, ISSN 2073-431X|
|Publication size in sheets||1.25|
|Keywords in English||distributed systems; distributed system modeling; asynchronous modeling; formal methods; model|
|Project||Development 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, end date 30-09-2019, II/2018/DS/1, Completed
|Score||= 15.0, 02-04-2020, ArticleFromJournal|
|Publication indicators||= 0; = 2|
|Citation count*||2 (2020-07-25)|
* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.