SAGE Verification Suite

Take a look at ReqV Tool, from the SAGE Verification Suite

Visit IDEA Lab Youtube Channel for more videos: link

Key Features

  • Automated consistency checking of requirements expressed in natural language.
  • Automated synthesis of high-level task-oriented optimal “correct-by-construction” policies (no verification needed).
  • Automated test generation and execution on black-box systems.


  • Requirement engineers without any knowledge related to formal methods.
  • Software developers without any knowledge of formal methods and logical languages.
  • System engineers interested to formally verify a model w.r.t. some properties.

Benefits for the User

  • Automated consistency checking of a set of requirements written in controlled natural language.
  • No prior knowledge related to specification languages is required to input the requirements (GUI support).
  • Human-readable feedback in the case of inconsistent requirements.
  • Test suite generated from a correct specification
  • Domain and application independent.


  • Set of requirements in natural (controlled English) language, formulated as PSPs for Linear Temporal Logic (LTL) extended to constrained numerical signals


  • Consistency result (yes/no). In the case of inconsistency, the tool returns the minimal set of requirements that causes the inconsistency.
  • Test report of the executed test suite.

Role in the CERBERO Toolchain

  • Requirements verification at the early stage of the design process

Tool Highlight

[Table: ReqV]


ReqV Brochure here

ReqT Brochure here

SpecPro Brochure here

Hydra Brochure here

Web Page






Return to Toolchain