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.

Users

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

Inputs

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

Outputs

• 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]

Brochure

ReqV Brochure here

ReqT Brochure here

SpecPro Brochure here

Hydra Brochure here

Web Page

ReqV

ReqT

SpecPro

Hydra

Return to Toolchain