An ontology-based approach to support formal verification of concurrent systems

Natalia Garanina, Igor Anureev, Elena Sidorova, Dmitry Koznov, Vladimir Zyubin, Sergei Gorlatch

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

Аннотация

Formal verification ensures the absence of design errors in a system with respect to system’s requirements. This is especially important for the control software of critical systems, ranging from automatic components of avionics and spacecrafts to modules of distributed banking transactions. In this paper, we present a verification support framework that enables automatic extraction of a concurrent system’s requirements from the technical documentation and formal verification of the system design using an external or built-in verification tool that checks whether the system meets the extracted requirements. Our support approach also provides visualization and editing options for both the system model and requirements. The key data components of our framework are ontological descriptions of the verified system and its requirements. We describe the methods used in our support framework and we illustrate their work for the use case of an automatic control system.

Язык оригиналаанглийский
Название основной публикацииFormal Methods- FM 2019 International Workshops - Revised Selected Papers
РедакторыEmil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, David Delmas
ИздательSpringer Nature
Страницы114-130
Число страниц17
ISBN (электронное издание)978-3-030-54994-7
ISBN (печатное издание)9783030549930
DOI
СостояниеОпубликовано - 1 сен 2020
Событие3rd World Congress on Formal Methods, FM 2019 - Porto, Португалия
Продолжительность: 7 окт 201911 окт 2019

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

НазваниеLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Том12232 LNCS
ISSN (печатное издание)0302-9743
ISSN (электронное издание)1611-3349

Конференция

Конференция3rd World Congress on Formal Methods, FM 2019
СтранаПортугалия
ГородPorto
Период07.10.201911.10.2019

Fingerprint Подробные сведения о темах исследования «An ontology-based approach to support formal verification of concurrent systems». Вместе они формируют уникальный семантический отпечаток (fingerprint).

  • Цитировать

    Garanina, N., Anureev, I., Sidorova, E., Koznov, D., Zyubin, V., & Gorlatch, S. (2020). An ontology-based approach to support formal verification of concurrent systems. В E. Sekerinski, N. Moreira, J. N. Oliveira, D. Ratiu, R. Guidotti, M. Farrell, M. Luckcuck, D. Marmsoler, J. Campos, T. Astarte, L. Gonnord, A. Cerone, L. Couto, B. Dongol, M. Kutrib, P. Monteiro, & D. Delmas (Ред.), Formal Methods- FM 2019 International Workshops - Revised Selected Papers (стр. 114-130). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Том 12232 LNCS). Springer Nature. https://doi.org/10.1007/978-3-030-54994-7_9