Model Checking Mutual Exclusion Algorithms Using UPPAAL

被引：1

作者：

Cicirelli, Franco ^{[1
]}

Nigro, Libero ^{[1
]}

Sciammarella, Paolo F. ^{[1
]}

机构：

[1] Univ Calabria, Dept Informat Modelling Elect & Syst Sci DIMES, Arcavacata Di Rende, CS, Italy

来源：

SOFTWARE ENGINEERING PERSPECTIVES AND APPLICATION IN INTELLIGENT SYSTEMS, VOL 2 | 2016年 / 465卷

关键词：

Mutual exclusion algorithms; Model checking; Timed automata; UPPAAL;

D O I：

10.1007/978-3-319-33622-0_19

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

This paper proposes an approach to modelling and exhaustive verification of mutual exclusion algorithms which is based on Timed Automata in the context of the popular UPPAAL toolbox. The approach makes it possible to study the properties of a mutual exclusion algorithm also in the presence of the time dimension. For demonstration purposes some historical algorithms are modelled and thoroughly analyzed, going beyond some informal reasoning reported in the literature. The paper also proposes a mutual exclusion algorithm for N >= 2 processes whose model checking confirms it satisfies all the required properties.

引用

页码：203 / 215

页数：13

共 50 条

[1] Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms
Katz, Gal
Peled, Doron
[J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2008, 5311 : 33 - 47
[2] Model Checking of TTCAN Protocol Using UPPAAL
Liu Shuxin
Yoshiura, Noriaki
[J]. COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2018, PT IV, 2018, 10963 : 550 - 564
[3] Model Checking of Needham-Schroeder Protocol Using UPPAAL
Rong, Mei
Li, Zhonghui
Zhang, Guangquan
[J]. 2010 6TH INTERNATIONAL CONFERENCE ON WIRELESS COMMUNICATIONS NETWORKING AND MOBILE COMPUTING (WICOM), 2010,
[4] Mutual Exclusion Algorithms in the Shared Queue Model
Wang, Junxing
Wang, Zhengyu
[J]. DISTRIBUTED COMPUTING AND NETWORKING, ICDCN 2014, 2014, 8314 : 29 - 43
[5] Model Checking for SpaceWire Link Interface Design Using Uppaal
Luo, Ping
Wang, Rui
Li, Xiaojuan
Guan, Yong
Zhang, Jie
Wei, Hongxing
[J]. 2013 IEEE 37TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSACW), 2013, : 181 - 186
[6] Comparison of Model Checking Tools Using Timed Automata - PRISM and UPPAAL
Naeem, Aaamir
Azam, Farooque
Amjad, Anam
Anwar, Muhammad Waseem
[J]. 2018 IEEE INTERNATIONAL CONFERENCE ON COMPUTER AND COMMUNICATION ENGINEERING TECHNOLOGY (CCET), 2018, : 248 - 253
[7] MODEL CHECKING KNOWLEDGE AND COMMITMENTS IN MULTIAGENT SYSTEMS USING ACTORS AND UPPAAL
Nigro, Christian
Nigro, Libero
Sciammarella, Paolo F.
[J]. 32ND EUROPEAN CONFERENCE ON MODELLING AND SIMULATION (ECMS 2018), 2018, : 136 - 142
[8] Model checking-based genetic programming with an application to mutual exclusion
Katz, Cal
Peled, Doren
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 141 - 156
[9] Towards Model Checking of Voting Protocols in UPPAAL
Jamroga, Wojciech
Kim, Yan
Kurpiewski, Damian
Ryan, Peter Y. A.
[J]. ELECTRONIC VOTING, E-VOTE-ID 2020, 2020, 12455 : 129 - 146
[10] Generic Algorithms for Consistency Checking of Mutual-Exclusion and Binding Constraints in a Business Process Context
Strembeck, Mark
Mendling, Jan
[J]. ON THE MOVE TO MEANINGFUL INTERNET SYSTEMS: OTM 2010, PT I, 2010, 6426 : 204 - +

← 1 2 3 4 5 →