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 proceedingConference contributionResearchpeer-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

Garanina, Natalia ; Koznov, Dmitry. / Static Checking Consistency of Temporal Requirements for Control Software. Advances in Model and Data Engineering in the Digitalization Era - MEDI 2021 International Workshops: DETECT, SIAS, CSMML, BIOC, HEDA, Proceedings. editor / Ladjel Bellatreche ; George Chernishev ; Antonio Corral ; Samir Ouchani ; Jüri Vain. Springer Nature, 2021. pp. 189-203 (Communications in Computer and Information Science).

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 -

ID: 88427575