Petri Net. Theory and applications

It is a key task of modern System-on-Chip (SoC) and Network-on-Chip (NoC) design to efficiently explore this design space regarding aspects like performance, flexibility and power consumption presumably in an early stage of the design flow in order to reduce design time and design costs. In this chapter several examples for modelling of on-chip communication using Petri Net based modelling techniques have been presented. These examples include modelling of internal processor communication and modelling of inter-processor communication using a crossbar switch fabric. For these examples deterministic and stochastic Petri Nets have been applied as modelling technique. More complex NoC communication has been modelled applying Coloured Petri Nets. The results obtained with all of these models were compared to those calculated on an FPGA based emulator. In all presented experiments the performance measures derived using these models showed a good precision compared to the results acquired using the FPGA based emulator. Furthermore, the Petri Net based results could be derived in attractively short modelling times with only moderate effort. Therefore, Petri Net based modelling of on-chip communication appears to be a very attractive approach to explore the design space of communication architectures in an early stage of the design process. DSPN based and CPN based modelling both provide specific advantages. DSPN models are suited for systems with moderate complexity such as communication systems with a small number of clients or bus based communication. The ease of modelling combined with the possibility of an analytical solution of the equations underlying the DSPN model provides a way to quickly obtain results. For more complex systems including a lot of data and complex functionalities, for example the addressing scheme and the routing algorithm in a NoC, CPN models are more adequate. DSPN based modelling of such systems is not as efficient since DSPNs do not provide a means of modelling data structures. As CPNs include data structures and allow to model complex behaviour in form of coloursets and transfer functions, CPN based modelling is well suited to analyze complex on-chip communication systems. Current topics in the field of NoC communication modelling to be addressed with Petri Net based methods are locating hotspots, analyzing quality-of-service aspects (data integrity, guaranteed service, etc.) and complex adaptive routing algorithms (incl. the checking of absence of deadlocks) In this chapter, we have presented time Petri Nets (TPNs) and a structural translation from TPNs to TA. Any TPN T and its associated TA (T) are timed bisimilar. Such a translation has many theoretical implications. Most of the positive theoretical results on TA carry over to TPNs. The class of TPNs can be extended by allowing strict constraints (open, half-open or closed intervals) to specify the firing dates of the transitions; for this extended class, the following results follow from our translation and from Theorem 5:? TCTL model checking is decidable for bounded TPNs. Moreover efficient algorithms used in U PPAAL (Pettersson and Larsen, 2000) and K RONOS (Yovine, 1997) are exact for the class of TA obtained with our translation;? it is decidable whether a TA is non-zeno or not (Henzinger et al., 1994) and thus our result provides a way to decide non-zenoness for bounded TPNs;? lastly, as our translation is structural, it is possible to use a model-checker to find sufficient conditions of unboundedness of the TPN. These results enable us to use algorithms and tools developed for TA to check quantitative properties on TPNs. For instance, it is possible to check real-time properties expressed in the logic TCTL on bounded TPNs. The tool R OMEO (Gardey et al., 2005) that has been developed for the analysis of TPN (state space computation and "on-the-fly" model-checking of reachability properties) implements this translation of a TPN into the equivalent TA in U PPAAL input format. Our approach turns out to be a good alternative to existing methods for verifying TPNs:? with our translation and U PPAAL we were able to check safety properties on very large TPNs that cannot be handled by other existing tools;? we also extend the class of properties that can be checked on TPNs to real-time quantitative properties. Note also that using our translation, we can take advantage of all the features of a tool like U PPAAL : looking for counter examples is usually much faster than checking a safety property. Moreover if a safety property is false, we will obtain a counter example even for unbounded TPNs (if we use breadth-first search). There are currently new features being developed for tools like R OMEO that enables one to directly check TCTL properties on a TPN without translating it into a TA. Aknowledgments The authors wish to thank Didier Lime for his careful reading of this chapter and useful comments to improve many parts of the text In this paper, we proposed a method to use SO-SAM to formally specify service-oriented application architectures modeled by an extension of UML? component and connector view. By doing so, we combine the benefit of UML? easy to comprehend and extensive tools support, and the analyzability of SO-SAM. The cost of our methods mainly comes from three parts: the construction of algebraic specifications, the generation of algebraic high-level nets from statechart diagrams, and the creation of temporal formulas from sequence diagrams. Since an algebraic specification is used to model the implied information of statechart diagrams, generally speaking we can generate operation and sort definitions of an algebraic specification automatically, but not for the relationships among these operations. The size of a generated algebraic specification is "linear" to the size of implied information. From our previous work [12], we know the generation of Petri nets from a statechart diagram can be fulfilled automatically for most cases, and a Petri net and the corresponding statechart diagram are at the same size. The generation of temporal logic formulas from sequence diagrams can be largely automated since the generation is very simple and straightforward. There are at least three immediate extensions to the work we have presented here. First, we intend to integrate the translation from UML architecture to SO-SAM with the mapping from SO-SAM to Maude so that some existing tool we have developed can be used for the model checking of system properties. And second, we intend to make effective use of the tools currently available for SAM model [21] to reason about the web specifications during the runtime. Finally, the translation into SO-SAM presented here must be extended in order to consider full application oriented view approach such as WSCI [4]; in particular, dealing with constructs such as correlations, transactions, properties and others, that have been omitted in this work. This extension would allow the analyzing on the more application oriented view approach using UML architecture descriptions