AutoReq: expressing and verifying requirements for control systems

TL;DR

AutoReq introduces a unified approach for writing and verifying control system requirements, ensuring consistency and correctness through formal methods, demonstrated on a landing gear system example.

Contribution

The paper presents AutoReq, a novel method that aligns requirements and implementation verification using formal techniques, improving accuracy and reducing errors.

Findings

Mechanical proof of requirement consistency

Uncovered an error in existing discussion

Validated approach on landing gear system

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.