OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

AutoReq: expressing and verifying requirements for control systems

Naumchev, Alexandr and Meyer, Bertrand and Mazzara, Manuel and Galinier, Florian and Bruel, Jean-Michel and Ebersold, Sophie AutoReq: expressing and verifying requirements for control systems. (2019) Journal of Visual Languages and Computing, 51. 131-142. ISSN 1045-926X

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1016/j.cola.2019.02.004


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.

Item Type:Article
HAL Id:hal-02878938
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Innopolis University (RUSSIA)
Other partners > Politecnico di Milano (ITALY)
Laboratory name:
Deposited On:17 Jun 2020 09:26

Repository Staff Only: item control page