Formal Relationship between Petri Nets and Graph Grammars as Basis for Animation Views in GenGED
Roswitha Bardohl, Claudia Ermel, Julia Padberg · 2002
Specification techniques like Petri nets al- low for the formal description and analysis of systems. Although tool support exists for many different Petri net classes and tasks, a domain-specific animation of net behav- ior, however, is not yet supported by many Petri net tools. In this contribution, we present a formal approach for the generic specification of several Petri net classes inclu d- ing animation views. The approach follows the notions of GenGED, a tool for the visual specification of visual lan- guages based on algebraic graph transformation. More- over, we give a proof of the semantical compatibility of Algebraic High-Level Petri nets and their representation a s graph grammars in GenGED. The proof is based on the for- mal semantics of Petri net behavior and the construction of graph derivations as pushouts in the category of graphs and graph morphisms. Visual modeling techniques are of growing interest for an application-oriented presentation of models given by a formal specification. Especially, for non-experts in forma l modeling, a layout of the model and its behavior simulation in the application domain would be desirable. Based on the GenGED approach for the generic specification of vi- sual languages (VLs), we define a relationship between the formal model of Petri nets and a so-called animation view by giving a layout for a model as icons in the application