MEA: A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity

Junfu Luo; Jiaqi Yin; Huibiao Zhu

doi:10.1007/978-3-031-29927-8_30

MEA: A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity

Junfu Luo, Jiaqi Yin, Huibiao Zhu

School of Software

East China Normal University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

The mutual exclusion problem is a classic and essential problem in computer science. Since its inception, many related algorithms and variants have been proposed. However, finding the atomicity requirement of mutual exclusion algorithms remains challenging. In this paper, we proposed a model-checking framework called MEA to solve this issue, which is implemented in Maude. MEA provides a workflow to model a mutual exclusion algorithm and can easily perform verification. We use two classic mutual exclusion algorithms as examples to elaborate on how it works. Both two cases denote that MEA is capable of basic modeling of mutual exclusion algorithms focusing on atomicity.

Original language	English
Title of host publication	Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings
Editors	Hiroyuki Takizawa, Hong Shen, Toshihiro Hanawa, Jong Hyuk Park, Hui Tian, Ryusuke Egawa
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	387-398
Number of pages	12
ISBN (Print)	9783031299261
DOIs	https://doi.org/10.1007/978-3-031-29927-8_30
State	Published - 2023
Event	23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022 - Sendai, Japan Duration: 7 Dec 2022 → 9 Dec 2022

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13798 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022
Country/Territory	Japan
City	Sendai
Period	7/12/22 → 9/12/22

Keywords

Atomicity
Maude
MEA
Model checking
Mutual exclusion algorithm

Access to Document

10.1007/978-3-031-29927-8_30

Cite this

Luo, J., Yin, J., & Zhu, H. (2023). MEA: A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity. In H. Takizawa, H. Shen, T. Hanawa, J. Hyuk Park, H. Tian, & R. Egawa (Eds.), Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings (pp. 387-398). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13798 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-29927-8_30

Luo, Junfu ; Yin, Jiaqi ; Zhu, Huibiao. / MEA : A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity. Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings. editor / Hiroyuki Takizawa ; Hong Shen ; Toshihiro Hanawa ; Jong Hyuk Park ; Hui Tian ; Ryusuke Egawa. Springer Science and Business Media Deutschland GmbH, 2023. pp. 387-398 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{eed9ff89c26749399fb11de51dbcd7ea,

title = "MEA: A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity",

abstract = "The mutual exclusion problem is a classic and essential problem in computer science. Since its inception, many related algorithms and variants have been proposed. However, finding the atomicity requirement of mutual exclusion algorithms remains challenging. In this paper, we proposed a model-checking framework called MEA to solve this issue, which is implemented in Maude. MEA provides a workflow to model a mutual exclusion algorithm and can easily perform verification. We use two classic mutual exclusion algorithms as examples to elaborate on how it works. Both two cases denote that MEA is capable of basic modeling of mutual exclusion algorithms focusing on atomicity.",

keywords = "Atomicity, Maude, MEA, Model checking, Mutual exclusion algorithm",

author = "Junfu Luo and Jiaqi Yin and Huibiao Zhu",

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022 ; Conference date: 07-12-2022 Through 09-12-2022",

year = "2023",

doi = "10.1007/978-3-031-29927-8_30",

language = "英语",

isbn = "9783031299261",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "387--398",

editor = "Hiroyuki Takizawa and Hong Shen and Toshihiro Hanawa and {Hyuk Park}, Jong and Hui Tian and Ryusuke Egawa",

booktitle = "Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings",

}

Luo, J, Yin, J & Zhu, H 2023, MEA: A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity. in H Takizawa, H Shen, T Hanawa, J Hyuk Park, H Tian & R Egawa (eds), Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13798 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 387-398, 23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022, Sendai, Japan, 7/12/22. https://doi.org/10.1007/978-3-031-29927-8_30

MEA: A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity. / Luo, Junfu; Yin, Jiaqi; Zhu, Huibiao.
Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings. ed. / Hiroyuki Takizawa; Hong Shen; Toshihiro Hanawa; Jong Hyuk Park; Hui Tian; Ryusuke Egawa. Springer Science and Business Media Deutschland GmbH, 2023. p. 387-398 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13798 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - MEA

T2 - 23rd International Conference on Parallel and Distributed Computing, Applications, and Technologies, PDCAT 2022

AU - Luo, Junfu

AU - Yin, Jiaqi

AU - Zhu, Huibiao

PY - 2023

Y1 - 2023

N2 - The mutual exclusion problem is a classic and essential problem in computer science. Since its inception, many related algorithms and variants have been proposed. However, finding the atomicity requirement of mutual exclusion algorithms remains challenging. In this paper, we proposed a model-checking framework called MEA to solve this issue, which is implemented in Maude. MEA provides a workflow to model a mutual exclusion algorithm and can easily perform verification. We use two classic mutual exclusion algorithms as examples to elaborate on how it works. Both two cases denote that MEA is capable of basic modeling of mutual exclusion algorithms focusing on atomicity.

AB - The mutual exclusion problem is a classic and essential problem in computer science. Since its inception, many related algorithms and variants have been proposed. However, finding the atomicity requirement of mutual exclusion algorithms remains challenging. In this paper, we proposed a model-checking framework called MEA to solve this issue, which is implemented in Maude. MEA provides a workflow to model a mutual exclusion algorithm and can easily perform verification. We use two classic mutual exclusion algorithms as examples to elaborate on how it works. Both two cases denote that MEA is capable of basic modeling of mutual exclusion algorithms focusing on atomicity.

KW - Atomicity

KW - Maude

KW - MEA

KW - Model checking

KW - Mutual exclusion algorithm

UR - http://www.scopus.com/inward/record.url?scp=85159396123&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-29927-8_30

DO - 10.1007/978-3-031-29927-8_30

M3 - 会议稿件

AN - SCOPUS:85159396123

SN - 9783031299261

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 387

EP - 398

BT - Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings

A2 - Takizawa, Hiroyuki

A2 - Shen, Hong

A2 - Hanawa, Toshihiro

A2 - Hyuk Park, Jong

A2 - Tian, Hui

A2 - Egawa, Ryusuke

PB - Springer Science and Business Media Deutschland GmbH

Y2 - 7 December 2022 through 9 December 2022

ER -

Luo J, Yin J, Zhu H. MEA: A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity. In Takizawa H, Shen H, Hanawa T, Hyuk Park J, Tian H, Egawa R, editors, Parallel and Distributed Computing, Applications and Technologies - 23rd International Conference, PDCAT 2022, Proceedings. Springer Science and Business Media Deutschland GmbH. 2023. p. 387-398. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-29927-8_30

MEA: A Framework for Model Checking of Mutual Exclusion Algorithms Focusing on Atomicity

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this