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' 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.

Publication
Journal of Visual Languages and Computing
Alexandr Naumchev
Alexandr Naumchev
2019 - Associate Professor at Innopolis University

Co-directed with Bertrand Meyer, Innopolis University.

Bertrand Meyer
Bertrand Meyer
Professor of Software Engineering
Florian Galinier
Florian Galinier
Ph.D. student since 09/2016

Co-directed with Bertrand Meyer and Sophie Ebersold

Jean-Michel Bruel
Jean-Michel Bruel
Professor of Software Engineering

My research interests include Model-Based Systems Engineering and Requirements Engineering.

Sophie Ebersold-Marcaillou
Sophie Ebersold-Marcaillou
Associate Professor of Software Engineering

Related