Standard

AutoReq: Expressing and verifying requirements for control systems. / Naumchev, Alexandr; Meyer, Bertrand; Mazzara, Manuel et al.

In: Journal of Computer Languages, Vol. 51, 01.04.2019, p. 131-142.

Research output: Contribution to journal › Article › peer-review

Harvard

Naumchev, A, Meyer, B, Mazzara, M, Galinier, F, Bruel, J-M & Ebersold, S 2019, 'AutoReq: Expressing and verifying requirements for control systems', Journal of Computer Languages, vol. 51, pp. 131-142. https://doi.org/10.1016/j.cola.2019.02.004

APA

Naumchev, A., Meyer, B., Mazzara, M., Galinier, F., Bruel, J-M., & Ebersold, S. (2019). AutoReq: Expressing and verifying requirements for control systems. Journal of Computer Languages, 51, 131-142. https://doi.org/10.1016/j.cola.2019.02.004

Vancouver

Naumchev A, Meyer B, Mazzara M, Galinier F, Bruel J-M, Ebersold S. AutoReq: Expressing and verifying requirements for control systems. Journal of Computer Languages. 2019 Apr 1;51:131-142. doi: 10.1016/j.cola.2019.02.004

Author

Naumchev, Alexandr ; Meyer, Bertrand ; Mazzara, Manuel et al. / AutoReq: Expressing and verifying requirements for control systems. In: Journal of Computer Languages. 2019 ; Vol. 51. pp. 131-142.

BibTeX

@article{8f637b413c3e40fb9b013ff17c5cf51d,
title = "AutoReq: Expressing and verifying requirements for control systems",
abstract = "The considerable effort of writing requirements is only worthwhile if the result meets two conditions: the requirements reflect stakeholders{\textquoteright} needs, and the implementation satisfies them. In usual approaches, the use of different notations for requirements (often natural language) and implementations (a programming language) makes both conditions elusive. AutoReq, presented in this article, takes a different approach to both the writing of requirements and their verification. Applying the approach to a well-documented example, a landing gear system, allowed for a mechanical proof of consistency and uncovered an error in a published discussion of the problem.",
keywords = "AUTOPROOF, SEAMLESS REQUIREMENTS, SPECIFICATION DRIVERS, AUTOREQ, DESIGN BY CONTRACT, EIFFEL, LANDING GEAR SYSTEM, MULTIREQUIREMENTS",
author = "Alexandr Naumchev and Bertrand Meyer and Manuel Mazzara and Florian Galinier and Jean-Michel Bruel and Sophie Ebersold",
note = "AutoReq: Expressing and verifying requirements for control systems / A. Naumchev, B. Meyer, M. Mazzara [et al.] // Journal of Computer Languages. – 2019. – Vol. 51. – P. 131-142. – DOI 10.1016/j.cola.2019.02.004.",
year = "2019",
month = apr,
day = "1",
doi = "10.1016/j.cola.2019.02.004",
language = "English",
volume = "51",
pages = "131--142",
journal = "Journal of Computer Languages",
issn = "2590-1184",
publisher = "Elsevier Science Publishing Company, Inc.",

}

RIS

TY - JOUR

T1 - AutoReq: Expressing and verifying requirements for control systems

AU - Naumchev, Alexandr

AU - Meyer, Bertrand

AU - Mazzara, Manuel

AU - Galinier, Florian

AU - Bruel, Jean-Michel

AU - Ebersold, Sophie

N1 - AutoReq: Expressing and verifying requirements for control systems / A. Naumchev, B. Meyer, M. Mazzara [et al.] // Journal of Computer Languages. – 2019. – Vol. 51. – P. 131-142. – DOI 10.1016/j.cola.2019.02.004.

PY - 2019/4/1

Y1 - 2019/4/1

N2 - The considerable effort of writing requirements is only worthwhile if the result meets two conditions: the requirements reflect stakeholders’ needs, and the implementation satisfies them. In usual approaches, the use of different notations for requirements (often natural language) and implementations (a programming language) makes both conditions elusive. AutoReq, presented in this article, takes a different approach to both the writing of requirements and their verification. Applying the approach to a well-documented example, a landing gear system, allowed for a mechanical proof of consistency and uncovered an error in a published discussion of the problem.

AB - The considerable effort of writing requirements is only worthwhile if the result meets two conditions: the requirements reflect stakeholders’ needs, and the implementation satisfies them. In usual approaches, the use of different notations for requirements (often natural language) and implementations (a programming language) makes both conditions elusive. AutoReq, presented in this article, takes a different approach to both the writing of requirements and their verification. Applying the approach to a well-documented example, a landing gear system, allowed for a mechanical proof of consistency and uncovered an error in a published discussion of the problem.

KW - AUTOPROOF

KW - SEAMLESS REQUIREMENTS

KW - SPECIFICATION DRIVERS

KW - AUTOREQ

KW - DESIGN BY CONTRACT

KW - EIFFEL

KW - LANDING GEAR SYSTEM

KW - MULTIREQUIREMENTS

UR - https://elibrary.ru/item.asp?id=38660066

UR - https://www.mendeley.com/catalogue/adf7a463-044e-31af-b2c5-812bb9435405/

U2 - 10.1016/j.cola.2019.02.004

DO - 10.1016/j.cola.2019.02.004

M3 - Article

VL - 51

SP - 131

EP - 142

JO - Journal of Computer Languages

JF - Journal of Computer Languages

SN - 2590-1184

ER -

ID: 65525274