Methods of Formal Software Verification in the Context of Distributed Systems

Anna Fatkina, Oleg Iakushkin, Dmitry Selivanov, Vladimir Korkhov

Результат исследований: Публикации в книгах, отчётах, сборниках, трудах конференцийстатья в сборнике материалов конференциинаучнаярецензирование

Выдержка

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.

Язык оригиналаанглийский
Название основной публикацииComputational Science and Its Applications – ICCSA 2019
Подзаголовок основной публикации19th International Conference, Saint Petersburg, Russia, July 1–4, 2019, Proceedings, Part II
Место публикацииCham
ИздательSpringer
Страницы546-555
ISBN (электронное издание)978-3-030-24296-1
ISBN (печатное издание)978-3-030-24295-4
DOI
СостояниеОпубликовано - 1 июл 2019
Событие19th International Conference on Computational Science and Its Applications, ICCSA 2019 - Saint Petersburg, Российская Федерация
Продолжительность: 1 июл 20194 июл 2019

Серия публикаций

НазваниеLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ИздательSpringer
Том11620
ISSN (печатное издание)0302-9743

Конференция

Конференция19th International Conference on Computational Science and Its Applications, ICCSA 2019
СтранаРоссийская Федерация
ГородSaint Petersburg
Период1/07/194/07/19

Отпечаток

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

Предметные области Scopus

  • Теоретические компьютерные науки
  • Компьютерные науки (все)

Цитировать

Fatkina, A., Iakushkin, O., Selivanov, D., & Korkhov, V. (2019). 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 (стр. 546-555). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Том 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. стр. 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. в 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), том. 11620, Springer, Cham, стр. 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. стр. 546-555 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Том 11620).

Результат исследований: Публикации в книгах, отчётах, сборниках, трудах конференцийстатья в сборнике материалов конференциинаучнаярецензирование

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. В Computational Science and Its Applications – ICCSA 2019: 19th International Conference, Saint Petersburg, Russia, July 1–4, 2019, Proceedings, Part II. Cham: Springer. 2019. стр. 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