AutoReq: expressing and verifying requirements for control systems
This addresses the problem of requirement verification for control systems, but appears incremental as it builds on existing formal methods.
The authors tackled the challenge of ensuring that control system requirements accurately reflect stakeholder needs and are satisfied by the implementation, by developing AutoReq, which allowed for a mechanical proof of consistency and uncovered an error in a published landing gear system example.
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.