Unfolding Shape Graphs


Sathyanathan, P.W. and Rensink, A. (2006) Unfolding Shape Graphs. [Report]

Abstract:Shape graphs have been introduced in [Ren04a, Ren04b] as an abstraction to be used in model checking object oriented software, where states of the system are represented as graphs. Intuitively, the graphs modeling the states represent the structure of objects dynamically allocated in the heap. State transitions are then generated by applying graph transformation rules corresponding to the statements of the program. Since the state space of such systems is potentially unbounded, the graphs representing the states are abstracted by shape graphs. Graph transformation systems may be analyzed [BCK01, BK02] by constructing finite structures that approximate their behaviour with arbitrary accuracy, by using techniques developed in the context of Petri nets. The approach of [BK02] is to construct a chain of finite under-approximations of the Winskel’s style unfolding of a graph grammar, as well as a chain of finite over-approximations of the unfolding, where both chains converge to the full unfolding. The approximations may then be used to check properties of the underlying graph transformation system. We apply this technique to approximate the behaviour of systems represented by shape graphs and graph tranformation rules.
Item Type:Report
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/66524
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 238695