SAGE Verification Suite
Take a look at ReqV Tool, from the SAGE Verification Suite
Visit IDEA Lab Youtube Channel for more videos: link
- 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
ReqV Brochure here
ReqT Brochure here
SpecPro Brochure here
Hydra Brochure here