@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",
}