VRS Tool

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:

ISS bullet
Checking of basic protocols set performed by Transition Consistency Checker
ISS bullet
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
ISS bullet
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.