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 Nature
Страницы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

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

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

Fingerprint Подробные сведения о темах исследования «Methods of Formal Software Verification in the Context of Distributed Systems». Вместе они формируют уникальный семантический отпечаток (fingerprint).

  • Цитировать

    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). Springer Nature. https://doi.org/10.1007/978-3-030-24296-1_43