Methods of Formal Software Verification in the Context of Distributed Systems

Anna Fatkina, Oleg Iakushkin, Dmitry Selivanov, Vladimir Korkhov

Research outputpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationComputational Science and Its Applications – ICCSA 2019
Subtitle of host publication19th International Conference, Saint Petersburg, Russia, July 1–4, 2019, Proceedings, Part II
Place of PublicationCham
PublisherSpringer
Pages546-555
ISBN (Electronic)978-3-030-24296-1
ISBN (Print)978-3-030-24295-4
DOIs
Publication statusPublished - 1 Jul 2019
Event19th International Conference on Computational Science and Its Applications, ICCSA 2019 - Saint Petersburg
Duration: 1 Jul 20194 Jul 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer
Volume11620
ISSN (Print)0302-9743

Conference

Conference19th International Conference on Computational Science and Its Applications, ICCSA 2019
CountryRussian Federation
CitySaint Petersburg
Period1/07/194/07/19

Fingerprint

Software Verification
Formal Verification
Distributed Systems
Automatic Verification
Programming
Verify
Range of data
Context
Formal verification

Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Fatkina, A., Iakushkin, O., Selivanov, D., & Korkhov, V. (2019). Methods of Formal Software Verification in the Context of Distributed Systems. In Computational Science and Its Applications – ICCSA 2019: 19th International Conference, Saint Petersburg, Russia, July 1–4, 2019, Proceedings, Part II (pp. 546-555). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11620). Cham: Springer. https://doi.org/10.1007/978-3-030-24296-1_43
Fatkina, Anna ; Iakushkin, Oleg ; Selivanov, Dmitry ; Korkhov, Vladimir. / Methods of Formal Software Verification in the Context of Distributed Systems. Computational Science and Its Applications – ICCSA 2019: 19th International Conference, Saint Petersburg, Russia, July 1–4, 2019, Proceedings, Part II. Cham : Springer, 2019. pp. 546-555 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{6f9f31ac7c3c41de8f829530553e7c0b,
title = "Methods of Formal Software Verification in the Context of Distributed Systems",
abstract = "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.",
keywords = "Coq, Distributed systems, Formal verification, Isabelle/HOL, Proof assistant, TLA+, Verdi",
author = "Anna Fatkina and Oleg Iakushkin and Dmitry Selivanov and Vladimir Korkhov",
note = "Fatkina A., Iakushkin O., Selivanov D., Korkhov V. (2019) Methods of Formal Software Verification in the Context of Distributed Systems. In: Misra S. et al. (eds) Computational Science and Its Applications – ICCSA 2019. ICCSA 2019. Lecture Notes in Computer Science, vol 11620. Springer, Cham",
year = "2019",
month = "7",
day = "1",
doi = "10.1007/978-3-030-24296-1_43",
language = "English",
isbn = "978-3-030-24295-4",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "546--555",
booktitle = "Computational Science and Its Applications – ICCSA 2019",
address = "Germany",

}

Fatkina, A, Iakushkin, O, Selivanov, D & Korkhov, V 2019, Methods of Formal Software Verification in the Context of Distributed Systems. in Computational Science and Its Applications – ICCSA 2019: 19th International Conference, Saint Petersburg, Russia, July 1–4, 2019, Proceedings, Part II. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11620, Springer, Cham, pp. 546-555, Saint Petersburg, 1/07/19. https://doi.org/10.1007/978-3-030-24296-1_43

Methods of Formal Software Verification in the Context of Distributed Systems. / Fatkina, Anna; Iakushkin, Oleg; Selivanov, Dmitry; Korkhov, Vladimir.

Computational Science and Its Applications – ICCSA 2019: 19th International Conference, Saint Petersburg, Russia, July 1–4, 2019, Proceedings, Part II. Cham : Springer, 2019. p. 546-555 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11620).

Research outputpeer-review

TY - GEN

T1 - Methods of Formal Software Verification in the Context of Distributed Systems

AU - Fatkina, Anna

AU - Iakushkin, Oleg

AU - Selivanov, Dmitry

AU - Korkhov, Vladimir

N1 - Fatkina A., Iakushkin O., Selivanov D., Korkhov V. (2019) Methods of Formal Software Verification in the Context of Distributed Systems. In: Misra S. et al. (eds) Computational Science and Its Applications – ICCSA 2019. ICCSA 2019. Lecture Notes in Computer Science, vol 11620. Springer, Cham

PY - 2019/7/1

Y1 - 2019/7/1

N2 - 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.

AB - 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.

KW - Coq

KW - Distributed systems

KW - Formal verification

KW - Isabelle/HOL

KW - Proof assistant

KW - TLA+

KW - Verdi

UR - http://www.scopus.com/inward/record.url?scp=85069165335&partnerID=8YFLogxK

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

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

M3 - Conference contribution

AN - SCOPUS:85069165335

SN - 978-3-030-24295-4

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 546

EP - 555

BT - Computational Science and Its Applications – ICCSA 2019

PB - Springer

CY - Cham

ER -

Fatkina A, Iakushkin O, Selivanov D, Korkhov V. Methods of Formal Software Verification in the Context of Distributed Systems. In Computational Science and Its Applications – ICCSA 2019: 19th International Conference, Saint Petersburg, Russia, July 1–4, 2019, Proceedings, Part II. Cham: Springer. 2019. p. 546-555. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-24296-1_43