SAGE Verification Suite
- Automated consistency checking of requirements expressed in natural language.
- Automated synthesis of high-level task-oriented optimal “correct-by-construction” policies (no verification needed).
- 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.
- 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.
Role in the CERBERO Toolchain
- Requirements verification at the early stage of the design process