Methods of Formal Software Verification in the Context of Distributed Systems

被引：2

作者：

Fatkina, Anna ^{[1
]}

Iakushkin, Oleg ^{[1
]}

Selivanov, Dmitry ^{[1
]}

Korkhov, Vladimir ^{[1
]}

机构：

[1] St Petersburg State Univ, St Petersburg, Russia

来源：

COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2019, PT II: 19TH INTERNATIONAL CONFERENCE, SAINT PETERSBURG, RUSSIA, JULY 1-4, 2019, PROCEEDINGS, PART II | 2019年 / 11620卷

关键词：

Formal verification; Proof assistant; TLA; Isabelle/HOL; Coq; Verdi; Distributed systems;

D O I：

10.1007/978-3-030-24296-1_43

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper discusses several formal verification instruments and compares them. These tools are Isabelle/HOL, Coq, Verdi, and TLA+. All of them are developed for automatic verification of distributed systems. However, there are a number of differences in implementation and application. Verdi provides an effortless way of implementation to verify some distributed systems. Isabelle/HOL and Coq, on the other hand, can solve a wider range of tasks. These provide a low-level interface and require programming skills. TLA+ allows the user to communicate in pseudocode-like language as well as per algorithm implementation in TLA+/PlusCal. It is the most versatile tool for formal verification which is considered in this paper.

引用

页码：546 / 555

页数：10

共 50 条

[21] Tutorial on formal methods for distributed and cooperative systems
Choppy, Christine
Haddad, Serge
Klaudel, Hanna
Kordon, Fabrice
Petrucci, Laure
Thierry-Mieg, Yarm
[J]. THEORETICAL ASPECTS OF COMPUTING - ICTAC 2006, 2006, 4281 : 362 - 365
[22] A symbolic model checking approach in formal verification of distributed systems
Souri, Alireza
Rahmani, Amir Masoud
Navimipour, Nima Jafari
Rezaei, Reza
[J]. HUMAN-CENTRIC COMPUTING AND INFORMATION SCIENCES, 2019, 9 (01):
[23] Model based formal verification of distributed production control systems
Kardos, M
Rammig, FJ
[J]. INTEGRATION OF SOFTWARE SPECIFICATION TECHNIQUES FOR APPLICATIONS IN ENGINEERING, 2004, 3147 : 451 - 473
[24] Reuse of components in formal modeling and verification of distributed control systems
Vyatkin, Valeriy
Hanisch, Hans-Michael
[J]. ETFA 2005: 10TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOL 1, PTS 1 AND 2, PROCEEDINGS, 2005, : 129 - 134
[25] Formal Specification and Verification of a Data Replication Approach in Distributed Systems
Souri, Alireza
[J]. INTERNATIONAL JOURNAL OF NEXT-GENERATION COMPUTING, 2016, 7 (01): : 18 - 37
[26] Formal Verification of UML Sequence Diagrams in the Embedded Systems Context
Cunha, E.
Custodio, M.
Rocha, H.
Barreto, R.
[J]. 2011 BRAZILIAN SYMPOSIUM ON COMPUTING SYSTEM ENGINEERING (SBESC), 2011, : 39 - 45
[27] A formal framework for context-aware systems specification and verification
Djoudi, Brahim
Bouanaka, Chafia
Zeghib, Nadia
[J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2016, 122 : 445 - 462
[28] FORMAL VERIFICATION OF CONCURRENT SOFTWARE
SCHNEIDER, FB
[J]. PROCEEDINGS : THE THIRTEENTH ANNUAL INTERNATIONAL COMPUTER SOFTWARE & APPLICATIONS CONFERENCE, 1989, : 59 - 59
[29] Context-aware payment for supply chains: Software architecture and formal verification
Zamani, Zahra
Bayat, Maryam
Moeini, Ali
Motevalian, Alireza
[J]. WORLD CONGRESS ON ENGINEERING 2008, VOLS I-II, 2008, : 211 - +
[30] Formal design and performance evaluation of parallel and distributed software systems
Goedicke, M
Meyer, T
[J]. SOFTWARE ENGINEERING FOR PARALLEL AND DISTRIBUTED SYSTEMS - INTERNATIONAL SYMPOSIUM PROCEEDINGS, 1998, : 136 - 144

← 1 2 3 4 5 →