Vom 20.12.2025 bis 11.01.2026 ist die Universitätsbibliothek geschlossen. Ab dem 12.01.2026 gelten wieder die regulären Öffnungszeiten. Ausnahme: Medizinische Hauptbibliothek und Zentralbibliothek sind bereits ab 05.01.2026 wieder geöffnet. Weitere Informationen
  • Formal modeling of a causal co...

Treffer: Formal modeling of a causal consistent distributed system and verification of its history via model checking using colored Petri net.

Title:
Formal modeling of a causal consistent distributed system and verification of its history via model checking using colored Petri net.
Authors:
Alsaegg KAM; Department of Computer Engineering, Faculty of Electrical and Computer Engineering, University of Tabriz, Tabriz, East Azerbijan, Iran., Pashazadeh S; Department of Information Technology, Faculty of Electrical and Computer Engineering, University of Tabriz, Tabriz, East Azerbaijan, Iran., Zolfy Lighvan M; Department of Computer Engineering, Faculty of Electrical and Computer Engineering, University of Tabriz, Tabriz, East Azerbijan, Iran.
Source:
PeerJ. Computer science [PeerJ Comput Sci] 2025 Jul 07; Vol. 11, pp. e2995. Date of Electronic Publication: 2025 Jul 07 (Print Publication: 2025).
Publication Type:
Journal Article
Language:
English
Journal Info:
Publisher: PeerJ Inc Country of Publication: United States NLM ID: 101660598 Publication Model: eCollection Cited Medium: Internet ISSN: 2376-5992 (Electronic) Linking ISSN: 23765992 NLM ISO Abbreviation: PeerJ Comput Sci Subsets: PubMed not MEDLINE
Imprint Name(s):
Original Publication: San Diego, CA : PeerJ Inc., [2015]-
References:
Sensors (Basel). 2022 Sep 14;22(18):. (PMID: 36146285)
Contributed Indexing:
Keywords: Causal consistency; Colored Petri net; Distributed system; Model checking; Modeling; Verification
Entry Date(s):
Date Created: 20250924 Date Completed: 20250924 Latest Revision: 20250926
Update Code:
20250926
PubMed Central ID:
PMC12453694
DOI:
10.7717/peerj-cs.2995
PMID:
40989378
Database:
MEDLINE

Weitere Informationen

Various consistency models for replicated distributed systems (DSs) have been developed and are usually implemented in the middleware layer. Causal consistency (CC) is a widely used consistency model appropriate for distributed applications like discussion groups and forums. One of the known distributed algorithms for CC is based on logical time synchronization with Fidge vector clocks that use the concepts of the hold-back and delivery queues for each replica. The basics of the algorithm and its assumptions are presented in the article. Then, a novel formal hierarchical colored Petri net model of a DS with CC support and three constituting replicas is presented. The proposed model operates based on the presented distributed algorithm for CC support with potential randomness for delays in message delivery. The article tries to answer the question: is a given distributed history (DH) a valid image of a causal-consistent distributed system (CCDS)? The proposed model validates a DH via model checking. The question is answered by the execution of the proposed model and the generation of its state space graph (SSG). Required model checking functions are developed for automatically analyzing SSG for (1) extracting the existence of the answer and (2) extraction of the shortest proof scenarios that can generate the given input DH. The model was used to analyze four case study examples. The article presents three effective techniques for decreasing the state space explosion problem. Results show that the colored Petri net model of a CCDS can automatically validate a DH using model checking.
(© 2025 Alsaegg et al.)

The authors declare that they have no competing interests.