Standard
An ontology-based approach to support formal verification of concurrent systems. / Garanina, Natalia; Anureev, Igor; Sidorova, Elena et al.
Formal Methods- FM 2019 International Workshops - Revised Selected Papers. ed. / 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, 2020. p. 114-130 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12232 LNCS).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
Harvard
Garanina, N, Anureev, I
, Sidorova, E, Koznov, D
, Zyubin, V & Gorlatch, S 2020,
An ontology-based approach to support formal verification of concurrent systems. in E Sekerinski, N Moreira, JN 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 (eds),
Formal Methods- FM 2019 International Workshops - Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12232 LNCS, Springer Nature, pp. 114-130, 3rd World Congress on Formal Methods, FM 2019, Porto, Portugal,
07.10.2019.
https://doi.org/10.1007/978-3-030-54994-7_9
APA
Garanina, N., Anureev, I.
, Sidorova, E., Koznov, D.
, Zyubin, V., & Gorlatch, S. (2020).
An ontology-based approach to support formal verification of concurrent systems. In 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 (Eds.),
Formal Methods- FM 2019 International Workshops - Revised Selected Papers (pp. 114-130). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12232 LNCS). Springer Nature.
https://doi.org/10.1007/978-3-030-54994-7_9
Vancouver
Garanina N, Anureev I
, Sidorova E, Koznov D
, Zyubin V, Gorlatch S.
An ontology-based approach to support formal verification of concurrent systems. In Sekerinski E, Moreira N, Oliveira JN, Ratiu D, Guidotti R, Farrell M, Luckcuck M, Marmsoler D, Campos J, Astarte T, Gonnord L, Cerone A, Couto L, Dongol B, Kutrib M, Monteiro P, Delmas D, editors, Formal Methods- FM 2019 International Workshops - Revised Selected Papers. Springer Nature. 2020. p. 114-130. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-54994-7_9
Author
Garanina, Natalia ; Anureev, Igor
; Sidorova, Elena et al. /
An ontology-based approach to support formal verification of concurrent systems. Formal Methods- FM 2019 International Workshops - Revised Selected Papers. editor / 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, 2020. pp. 114-130 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
BibTeX
@inproceedings{3724400f50154ed58215a9b989f36cd2,
title = "An ontology-based approach to support formal verification of concurrent systems",
abstract = "Formal verification ensures the absence of design errors in a system with respect to system{\textquoteright}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{\textquoteright}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.",
keywords = "Formal semantics, Formal verification, Information extraction, Ontology, Requirement engineering",
author = "Natalia Garanina and Igor Anureev and Elena Sidorova and Dmitry Koznov and Vladimir Zyubin and Sergei Gorlatch",
year = "2020",
month = sep,
day = "1",
doi = "10.1007/978-3-030-54994-7_9",
language = "English",
isbn = "9783030549930",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Nature",
pages = "114--130",
editor = "Emil Sekerinski and Nelma Moreira and Oliveira, {Jos{\'e} N.} and Daniel Ratiu and Riccardo Guidotti and Marie Farrell and Matt Luckcuck and Diego Marmsoler and Jos{\'e} Campos and Troy Astarte and Laure Gonnord and Antonio Cerone and Luis Couto and Brijesh Dongol and Martin Kutrib and Pedro Monteiro and David Delmas",
booktitle = "Formal Methods- FM 2019 International Workshops - Revised Selected Papers",
address = "United States",
note = "3rd World Congress on Formal Methods, FM 2019 ; Conference date: 07-10-2019 Through 11-10-2019",
}
RIS
TY - GEN
T1 - An ontology-based approach to support formal verification of concurrent systems
AU - Garanina, Natalia
AU - Anureev, Igor
AU - Sidorova, Elena
AU - Koznov, Dmitry
AU - Zyubin, Vladimir
AU - Gorlatch, Sergei
PY - 2020/9/1
Y1 - 2020/9/1
N2 - 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.
AB - 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.
KW - Formal semantics
KW - Formal verification
KW - Information extraction
KW - Ontology
KW - Requirement engineering
UR - http://www.scopus.com/inward/record.url?scp=85089716201&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-54994-7_9
DO - 10.1007/978-3-030-54994-7_9
M3 - Conference contribution
AN - SCOPUS:85089716201
SN - 9783030549930
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 114
EP - 130
BT - Formal Methods- FM 2019 International Workshops - Revised Selected Papers
A2 - Sekerinski, Emil
A2 - Moreira, Nelma
A2 - Oliveira, José N.
A2 - Ratiu, Daniel
A2 - Guidotti, Riccardo
A2 - Farrell, Marie
A2 - Luckcuck, Matt
A2 - Marmsoler, Diego
A2 - Campos, José
A2 - Astarte, Troy
A2 - Gonnord, Laure
A2 - Cerone, Antonio
A2 - Couto, Luis
A2 - Dongol, Brijesh
A2 - Kutrib, Martin
A2 - Monteiro, Pedro
A2 - Delmas, David
PB - Springer Nature
T2 - 3rd World Congress on Formal Methods, FM 2019
Y2 - 7 October 2019 through 11 October 2019
ER -
