The Verification of Requirements Specification (VRS) system was developed by ISS based on the theory of insertion modeling and algebraic programming initially created in Glushkov Institute of Cybernetics to perform the following tasks in the process of development of correct requirements specification:
Given set of formalized requirements - for software or hardware to automatically detect whether this set is consistent and complete with respect to certain criteria |
|
In case of detected inconsistency and/or incompleteness - to point out the particular causes of this in terms of the original requirements |
The VRS system performs these tasks using the following features:
Checking of basic protocols set performed by Transition Consistency Checker |
|
Using the Trace Generator to generate traces and scenarios from initial set of basic protocols and check systems for safety conditions, possible dead-locks, and reachability of given states of the system |
|
| Enabling the user to express local properties of a system that could be written as annotations for SDL and MSC scenarios and checked with Annotations Checker |
The system is compatible with Telelogic Tau 2.5 w.r.t. input data.