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

Original languageEnglish
Title of host publicationFormal Methods- FM 2019 International Workshops - Revised Selected Papers
EditorsEmil 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
PublisherSpringer Nature
Pages114-130
Number of pages17
ISBN (Print)9783030549930
DOIs
StatePublished - 2020
Event3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal
Duration: 7 Oct 201911 Oct 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12232 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd World Congress on Formal Methods, FM 2019
Country/TerritoryPortugal
CityPorto
Period7/10/1911/10/19

    Research areas

  • Formal semantics, Formal verification, Information extraction, Ontology, Requirement engineering

    Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

ID: 88427816