VRS is an acronym for “Verification of Requirement Specification”. This project is being developed at the Information Software System (ISS) – a research organization in Kiev contracted by Motorola.
VRS is a tool for deductive verification of requirements and specifications for software systems expressed in terms of MSC language. An extension mMSC of a standard MSC language is used as an input language of the system. VRS provides automatic checking of time consistency of MSC diagrams, consistency and completeness of basic protocols, correct use of basic protocols for building scenario, annotation consistency of scenario. The main application domains for the use of VRS are: modeling and simulation, real time applications, telecommunication systems.
Input information for the system is represented by means of three kinds of MSC diagrams:
Basic protocols
Such protocols are basic MSC diagrams supplemented with two sets of conditions. The conditions from the first set are called preconditions and are placed just after initialization of instances involved to these conditions. The conditions from the second set are called post-conditions and are placed just before termination of corresponding instances. Basic protocols are used to define generic meaning of messages and local actions. For such messages and local actions used in scenarios the following temporal constraints must hold: if preconditions are valid at some moment of time then corresponding protocol can be executed and the post-conditions are valid after the execution. Note that basic protocols can be parameterized. In this case different copies of the same protocol can be used in different places of scenario.
Basic protocols Scenarios
They are MSC diagrams, which use messages and local actions described in basic protocols. In-line expressions and references can be used in scenarios. Special conditions called annotations can be included in scenarios. These conditions are used to present various properties of systems under construction such as safety properties, efficiency properties, liveness, etc.
Independent diagrams
These diagrams do not refer to basic protocols and as a rule are used independently to define the set of traces (tests) with time specifications.
Types of properties verifiable in VRS
VRS is a tool that helps verify properties of MSC diagrams using automatic logic deduction. There are the following types of properties verifiable in VRS:
The verified property can be proved, not proved or refuted. In the case of negative result (not proved or refutation) the traces witnessing this result are generated as the output. Such a witnessing trace ends by a state where annotation condition cannot be proved or is refuted, or time constraint is not consistent with event ordering.
Transition consistency of basic protocols
The behavior of a system presented by a scenario and basic protocols can be described as a process of matching of messages and local actions defined in the scenario with the same messages and local actions defined in the basic protocols. At each step of this matching the selection of a basic protocol applicable in the current system state must be done. The applicability means that all preconditions are true in a given state. If we want to construct deterministic system then the selection of a protocol must depend only on the action (message or local action), which can be initially performed when a protocol starts (starting action). Therefore each time when some protocol can be applied, there must be only one protocol, which is applicable at this point. This property of basic protocols is called transition consistency. The applicability of a protocol depends on the current values of state variables and is checked by validating the preconditions of a protocol. The sufficient condition for this type of consistency can be formulated as follows. If preconditions of two basic protocols are intersected, that is the negation of their conjunction cannot be proved or can be refuted, then the processes defined by these protocols must be equivalent as well as their post-conditions.
Completeness of basic protocols
This property informally means that at any moment of time there must be at least one basic protocol that is applicable unless the scenario has not terminated. Sufficient condition for this is that the disjunction of all preconditions of all basic protocols is valid. Actually this condition is too strong and it can be weakened if some admissibility condition is given for a group of protocols. In this case the disjunction of preconditions of protocols for this group must be valid if the admissibility condition for this group is valid too.
Annotation consistency of scenarios
This property assumes that annotations in scenarios must be valid at corresponding states in any admissible scenarios execution.
To check the annotation consistency symbolic simulation of MSC diagrams is used rather than execution with specific states. Each time when annotations are met they are checked to be the consequences from current conditions. In the case of loops annotations can be used as loop invariants.
Time consistency
Each MSC diagram defines some partial order on the set of events, which can happen during its execution. This ordering must be consistent with time specifications, which should not destroy the original partial order of untimed MSC. This condition is known as time consistency of a diagram. To prove time consistency, the methods of solving linear constraints over reals are used.