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

PDF
365kB 
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 underapproximations of the Winskel’s style unfolding of a graph grammar, as well as a chain of finite overapproximations 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 
Faculty:  Electrical Engineering, Mathematics and Computer Science (EEMCS) 
Research Group:  
Link to this item:  http://purl.utwente.nl/publications/66524 
Export this item as:  BibTeX EndNote HTML Citation Reference Manager 
Repository Staff Only: item control page
Metis ID: 238695