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 条

[1] Tableau methods for formal verification of multi-agent distributed systems
Massacci, F
[J]. JOURNAL OF LOGIC AND COMPUTATION, 1998, 8 (03) : 373 - 400
[2] FORMAL SPECIFICATION AND VERIFICATION OF DISTRIBUTED SYSTEMS
CHEN, BS
YEH, RT
[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1983, 9 (06) : 710 - 722
[3] Towards Ontology-Based Formal Verification Methods for Context Aware Systems
Schmidtke, Hedda R.
Woo, Woontack
[J]. PERVASIVE COMPUTING, PROCEEDINGS, 2009, 5538 : 309 - 326
[4] Abstraction and Idealization in the Formal Verification of Software Systems
Angius, Nicola
[J]. MINDS AND MACHINES, 2013, 23 (02) : 211 - 226
[5] Abstraction and Idealization in the Formal Verification of Software Systems
Nicola Angius
[J]. Minds and Machines, 2013, 23 : 211 - 226
[6] A Formal Approach for Modeling and Verification of Distributed Systems
Ren, Gang
Deng, Pan
Yang, Chao
Zhang, Jianwei
Hua, Qingsong
[J]. CLOUD COMPUTING (CLOUDCOMP 2015), 2016, 167 : 317 - 322
[7] Formal methods and social context in software development
Goguen, JA
Luqi
[J]. TAPSOFT '95: THEORY AND PRACTICE OF SOFTWARE DEVELOPMENT, 1995, 915 : 62 - 81
[8] Formal methods for verification and validation of distributed interacting devices
Schmiedekamp, Mendel
Skarbez, Richard
Phoha, Shashi
[J]. PROCEEDINGS OF THE 10TH IASTED INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND APPLICATIONS, 2006, : 313 - +
[9] Efficient Modelling of Embedded Software Systems and Their Formal Verification
Estivill-Castro, Vladimir
Hexel, Rene
Rosenblueth, David A.
[J]. 2012 19TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), VOL 1, 2012, : 428 - 433
[10] Formal Verification of a Microkernel Used in Dependable Software Systems
Baumann, Christoph
Beckert, Bernhard
Blasum, Holger
Bormer, Thorsten
[J]. COMPUTER SAFETY, RELIABILITY, AND SECURITY, PROCEEDINGS, 2009, 5775 : 187 - +

← 1 2 3 4 5 →