Standard
Static Checking Consistency of Temporal Requirements for Control Software. / Garanina, Natalia; Koznov, Dmitry.
Advances in Model and Data Engineering in the Digitalization Era - MEDI 2021 International Workshops: DETECT, SIAS, CSMML, BIOC, HEDA, Proceedings. ed. / Ladjel Bellatreche; George Chernishev; Antonio Corral; Samir Ouchani; Jüri Vain. Springer Nature, 2021. p. 189-203 (Communications in Computer and Information Science; Vol. 1481 CCIS).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
Harvard
Garanina, N
& Koznov, D 2021,
Static Checking Consistency of Temporal Requirements for Control Software. in L Bellatreche, G Chernishev, A Corral, S Ouchani & J Vain (eds),
Advances in Model and Data Engineering in the Digitalization Era - MEDI 2021 International Workshops: DETECT, SIAS, CSMML, BIOC, HEDA, Proceedings. Communications in Computer and Information Science, vol. 1481 CCIS, Springer Nature, pp. 189-203, 10th International Conference on New Trends in Model and Data Engineering, MEDI 2021 held with 4th International Workshop on Modeling, Verification and Testing of Dependable Critical Systems, DETECT 2021, Symposium on Intelligent and Autonomous Systems, SIAS 2021, 1st Workshop on Control Software: Methods, Models, and Languages, CSMML 2021, Workshop on Blockchain for Inter-Organizational Collaboration, BIOC 2021 and 1st International Health Data Workshop, HEDA 2021, Virtual, Online,
21/06/21.
https://doi.org/10.1007/978-3-030-87657-9_15
APA
Garanina, N.
, & Koznov, D. (2021).
Static Checking Consistency of Temporal Requirements for Control Software. In L. Bellatreche, G. Chernishev, A. Corral, S. Ouchani, & J. Vain (Eds.),
Advances in Model and Data Engineering in the Digitalization Era - MEDI 2021 International Workshops: DETECT, SIAS, CSMML, BIOC, HEDA, Proceedings (pp. 189-203). (Communications in Computer and Information Science; Vol. 1481 CCIS). Springer Nature.
https://doi.org/10.1007/978-3-030-87657-9_15
Vancouver
Garanina N
, Koznov D.
Static Checking Consistency of Temporal Requirements for Control Software. In Bellatreche L, Chernishev G, Corral A, Ouchani S, Vain J, editors, Advances in Model and Data Engineering in the Digitalization Era - MEDI 2021 International Workshops: DETECT, SIAS, CSMML, BIOC, HEDA, Proceedings. Springer Nature. 2021. p. 189-203. (Communications in Computer and Information Science).
https://doi.org/10.1007/978-3-030-87657-9_15
Author
BibTeX
@inproceedings{01089ea7086a4c03948b5860a8b63c98,
title = "Static Checking Consistency of Temporal Requirements for Control Software",
abstract = "In this paper, we propose an approach to checking consistency of control software requirements described using pattern-based notation. This approach can be used at the beginning of control software verification to effectively identify contradicting and incompatible requirements. In this framework, we use pattern-based Event-Driven Temporal Logic (EDTL) to formalize the requirements. A set of requirements is represented as a set of EDTL-patterns which formal semantics defined by formulas of linear-time temporal logic LTL. Based on this semantics, we define the notion of requirement inconsistency and describe restrictions on the values of pattern attributes which make requirements inconsistent. Checking algorithm takes as an input pairs of requirements and compare their attributes. Its output is sets of consistent, inconsistent and incomparable requirements.",
keywords = "Formal semantics, Linear temporal logic, Requirement consistency, Requirement engineering",
author = "Natalia Garanina and Dmitry Koznov",
note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 10th International Conference on New Trends in Model and Data Engineering, MEDI 2021 held with 4th International Workshop on Modeling, Verification and Testing of Dependable Critical Systems, DETECT 2021, Symposium on Intelligent and Autonomous Systems, SIAS 2021, 1st Workshop on Control Software: Methods, Models, and Languages, CSMML 2021, Workshop on Blockchain for Inter-Organizational Collaboration, BIOC 2021 and 1st International Health Data Workshop, HEDA 2021 ; Conference date: 21-06-2021 Through 23-06-2021",
year = "2021",
doi = "10.1007/978-3-030-87657-9_15",
language = "English",
isbn = "9783030876562",
series = "Communications in Computer and Information Science",
publisher = "Springer Nature",
pages = "189--203",
editor = "Ladjel Bellatreche and George Chernishev and Antonio Corral and Samir Ouchani and J{\"u}ri Vain",
booktitle = "Advances in Model and Data Engineering in the Digitalization Era - MEDI 2021 International Workshops",
address = "Germany",
}
RIS
TY - GEN
T1 - Static Checking Consistency of Temporal Requirements for Control Software
AU - Garanina, Natalia
AU - Koznov, Dmitry
N1 - Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - In this paper, we propose an approach to checking consistency of control software requirements described using pattern-based notation. This approach can be used at the beginning of control software verification to effectively identify contradicting and incompatible requirements. In this framework, we use pattern-based Event-Driven Temporal Logic (EDTL) to formalize the requirements. A set of requirements is represented as a set of EDTL-patterns which formal semantics defined by formulas of linear-time temporal logic LTL. Based on this semantics, we define the notion of requirement inconsistency and describe restrictions on the values of pattern attributes which make requirements inconsistent. Checking algorithm takes as an input pairs of requirements and compare their attributes. Its output is sets of consistent, inconsistent and incomparable requirements.
AB - In this paper, we propose an approach to checking consistency of control software requirements described using pattern-based notation. This approach can be used at the beginning of control software verification to effectively identify contradicting and incompatible requirements. In this framework, we use pattern-based Event-Driven Temporal Logic (EDTL) to formalize the requirements. A set of requirements is represented as a set of EDTL-patterns which formal semantics defined by formulas of linear-time temporal logic LTL. Based on this semantics, we define the notion of requirement inconsistency and describe restrictions on the values of pattern attributes which make requirements inconsistent. Checking algorithm takes as an input pairs of requirements and compare their attributes. Its output is sets of consistent, inconsistent and incomparable requirements.
KW - Formal semantics
KW - Linear temporal logic
KW - Requirement consistency
KW - Requirement engineering
UR - http://www.scopus.com/inward/record.url?scp=85117486168&partnerID=8YFLogxK
UR - https://www.mendeley.com/catalogue/b38d1ec1-8e50-3478-8351-75ebbfd9362e/
U2 - 10.1007/978-3-030-87657-9_15
DO - 10.1007/978-3-030-87657-9_15
M3 - Conference contribution
AN - SCOPUS:85117486168
SN - 9783030876562
T3 - Communications in Computer and Information Science
SP - 189
EP - 203
BT - Advances in Model and Data Engineering in the Digitalization Era - MEDI 2021 International Workshops
A2 - Bellatreche, Ladjel
A2 - Chernishev, George
A2 - Corral, Antonio
A2 - Ouchani, Samir
A2 - Vain, Jüri
PB - Springer Nature
T2 - 10th International Conference on New Trends in Model and Data Engineering, MEDI 2021 held with 4th International Workshop on Modeling, Verification and Testing of Dependable Critical Systems, DETECT 2021, Symposium on Intelligent and Autonomous Systems, SIAS 2021, 1st Workshop on Control Software: Methods, Models, and Languages, CSMML 2021, Workshop on Blockchain for Inter-Organizational Collaboration, BIOC 2021 and 1st International Health Data Workshop, HEDA 2021
Y2 - 21 June 2021 through 23 June 2021
ER -