IBM
Contents Index Previous Next



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:

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
Contents Index Previous Next