![]() |
![]() |
![]() |
![]() |
![]() |
Validating Systems That Use the Ref Generator
The Ref generator (see The Ref Generator) is used to create pointer structures to be used in SDL systems. The Explorer supports the Ref generator, but imposes some restrictions on the usage of it due to the special requirements caused by state space exploration.
Variables that are defined to be Ref's to something can be used in two ways, either as a pointer to some other variable or as a pointer to a dynamically allocated memory area. Both ways of using Ref types are supported by the Explorer.
To handle dynamically allocated data areas the Explorer creates a special data structure as part of each system state. This data structure is a list of all data areas allocated by Alloc (the Ref operator that allocates a new data area) and data areas allocated in external C code (see Validating Systems with External C Code). The list contains for each data area in addition to the area itself information about e.g. the sort of the data area and the size of the data area. Whenever the Explorer copies a system state, the list of dynamically allocated data areas is also copied and all Ref variables are set up corresponding to the new copy of the list.
Some restrictions/simplifications are needed when using Ref sorts in the Explorer:
- Variables may not be defined to be of the VoidStar or VoidStarStar sorts, since the Explorer needs to know the sort and size of what is pointed to. This is not known for VoidStar and VoidStarStar sorts.
- A simplification is made when comparing two system states for equivalence (both in exhaustive exploration and in the hash function used by bit state exploration): Two Ref variables are considered equivalent if the data they are pointing to are equivalent. This may in some cases prune the search in situations where it should not have been pruned. Note that equivalence tests in the SDL system works correctly, if two Ref variables are compared using `=' they are considered the same only if they contain the same pointer value.
Note that the handling of pointers in the Explorer introduces a significant overhead that unfortunately reduces the number of transitions per second that is executed by the Explorer.
When performing state space exploration, the Explorer checks the usage of Ref variables when copying system states and reports several different types of problems including:
For more information about the reports see REF Errors.
http://www.ibm.com/rational |
![]() |
![]() |
![]() |
![]() |