Model Checking using Spin and SpinRCP

被引：0

作者：

Brezocnik, Zmago ^{[1
]}

Vlaovic, Bostjan ^{[1
]}

Vreze, Aleksander ^{[1
]}

机构：

[1] Univ Maribor, Fac Elect Engn & Comp Sci, Maribor, Slovenia

来源：

INFORMACIJE MIDEM-JOURNAL OF MICROELECTRONICS ELECTRONIC COMPONENTS AND MATERIALS | 2013年 / 43卷 / 04期

关键词：

formal verification; model checking; modelling; simulation; Promela; Spin; SpinRCP;

D O I：

暂无

中图分类号：

TM [电工技术]; TN [电子技术、通信技术];

学科分类号：

0808 ; 0809 ;

摘要：

Spin is one of the leading verification tools for the model checking of distributed systems. It is used over a broad spectrum of applications where systems can be represented as asynchronously running processes. This paper provides an overview of the concepts of model checking, the Spin model checker together with its input language Promela, and of the available graphical user interfaces to Spin. In order to offer Spin users an integrated development environment for Spin, we have developed a SpinRCP. We introduce its structure and demonstrate some of its features by considering a standard algorithm for leader election in a unidirectional ring.

引用

页码：235 / 250

页数：16

共 50 条

[1] Using SPIN model checking for flight software verification
Glück, PR
Holzmann, GJ
[J]. 2002 IEEE AEROSPACE CONFERENCE PROCEEDINGS, VOLS 1-7, 2002, : 105 - 113
[2] SPIN model checking: An introduction
Holzmann G.
Najm E.
Serhrouchni A.
[J]. International Journal on Software Tools for Technology Transfer, 2000, Springer Verlag (02) : 321 - 327
[3] Model Checking Paxos in Spin
Delzanno, Giorgio
Tatarek, Michele
Traverso, Riccardo
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (161): : 131 - 146
[4] Software model checking with SPIN
Holzmann, GJ
[J]. ADVANCES IN COMPUTERS, VOL 65, 2005, 65 : 77 - 108
[5] Model checking SDL with spin
Bosnacki, D
Dams, D
Holenderski, L
Sidorova, N
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2000, 1785 : 363 - 377
[6] Model Checking the IKEv2 Protocol Using Spin
Ninet, Tristan
Legay, Axel
Maillard, Romaric
Traonouez, Louis-Marie
Zendra, Olivier
[J]. 2019 17TH INTERNATIONAL CONFERENCE ON PRIVACY, SECURITY AND TRUST (PST), 2019, : 288 - 294
[7] Model checking in practice: Analysis of Generic Bootloader using SPIN
Das Barman, Kuntal
Mukhopadhyay, Debapriyay
[J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2007, 4789 : 232 - +
[8] αSPIN: A tool for abstract model checking
María del Mar Gallardo
Jesús Martínez
Pedro Merino
Ernesto Pimentel
[J]. International Journal on Software Tools for Technology Transfer, 2004, 5 (2-3) : 165 - 184
[9] SPIN Model Checking for the BEE System
Yamada, Chikatoshi
Ganti, Sudhakar
Miller, D. Michael
[J]. TENCON 2015 - 2015 IEEE REGION 10 CONFERENCE, 2015,
[10] Model checking active networks with SPIN
Gallardo, MD
Martínez, J
Merino, P
[J]. COMPUTER COMMUNICATIONS, 2005, 28 (06) : 609 - 622

← 1 2 3 4 5 →