SAGE Verification Suite

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

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

Role in the CERBERO Toolchain

  • Requirements verification at the early stage of the design process

Tool Highlight

[Table: ReqV]

Web Page

ReqV

SMarTplan