Mobile systems explore the interplay between locality and connectivity. A subsystem may have a connection to a remote subsystem and use this for communication. It may be necessary or desirable to move the subsystem close to the other in order to communicate. Alternatively, the method of communication may vary depending on proximity. This paper reviews a Petri Net formalisation for mobile systems which is intended to harness the intuitive graphical representation of Petri Nets and the long history of associated analysis techniques.The main contribution of the current paper is to assess the above formalism by using it to model and simulate Mobile IP, an Internet standard which caters for mobile nodes using IP version 4 addresses. These addresses indicate a fixed point of connection to the internet and the protocol caters for nodes being away from home. By defining the model as a Mobile Petri Net, the graphical notation helps to convey the flow of information, and the executable nature of the model opens the way to simulation, state space exploration and model checking.
Object-based systems present particular challenges for state space exploration. Objects can be dynamically created and discarded, and can be referenced via object identifiers. Consistent relabelling of object identifiers in a state leads to a state that is superficially different but behaviourally equivalent to the original. Similarly, object-based systems can include garbage Ñ objects which cannot be accessed from the root instance and cannot affect it. The presence of garbage can also result in unnecessary differentiation of states. Both of these factors can lead to state space explosion. This paper defines object-based systems based on the Petri Net formalism and considers both equivalence reduction and the sweep-line method for exploring the state space of such systems. Experimental results are presented for the case study of a communication protocol. .
Mobile systems explore the interplay between locality and connectivity. A subsystem may have a connection to a remote subsystem and use this for communication. Alternatively, it may be necessary or desirable to move the subsystem close to the other in order to communicate. This paper presents a Petri Net formalisation of mobile systems so as to harness the intuitive graphical representation of Petri Nets and the long history of associated analysis techniques. The proposed formalism starts with modular Petri Nets, where a net is divided into modules which can interact via place and transition fusion. The first change is that the flat module structure is replaced by fully nested modules, called locations. The nesting of locations provides a notion of locality while their fusion context determines their connectivity. The transitions constituting a location are constrained so that we can determine when a location is occupied by a subsystem, and when the subsystem shifts from one location to another. We present both a colourless and a coloured version of the formalism. The colourless version is conceptually simpler, while the coloured version makes it easier to identify isolated subsystems for which garbage collection may be appropriate..
In this article, we present a practical analysis approach that makes use of the modular nature of component-based designs to alleviate the state space explosion problem, a well-known obstacle to system verification. The key is to specify interaction protocols for components using a lightweight formal language and then to utilise these protocols as contracts for independent analysis of the components and their interactions. These protocols are often missing or informally documented. It is demonstrated how consistency properties of closed and open component-based designs can be verified using this divide-and-conquer approach.
In this paper, we introduce a component-based design methodology and present a practical analysis approach that makes use of the modular nature of component-based designs to alleviate the state space explosion problem, a wellknown obstacle to system verification. In addition, the approach is illustrated by application to a non-trivial case study: the production cell. It is shown that not only the basic consistency property, viz. the freedom from unexpected reception and deadlock, but also other important safety properties in the design can be proved.
Process networks are popular for modelling distributed computing and signal processing applications, and multi-processor architectures. At the architecture description level, they have the flexibility to model actual processes using various formalisms. This is especially important where the systems are composed of parts with different characteristics, e.g. control-based or datafloworiented. However, this heterogeneity of processes presents a challenge for the analysis of process networks. This research proposes a lightweight method for analysing properties of such networks, such as freedom from unexpected reception and deadlock. The method employs interface automata as a bridge between the architectural model and heterogeneous processes. Thus, the properties are determined by a series of small tasks at both the architecture level and the process level. This separation of concerns simplifies the handling of heterogeneous processes and alleviates the potential state space explosion problem when analysing large systems.
Process networks are a popular modelling technique for distributed computing and signal processing applications. The ability to support various parallelism or communication patterns also makes them suitable for modelling multi-processor architectures. At the architecture description level, the language provides the flexibility to model actual processes using various formalisms. This is especially important when the systems are comprised of parts with distinct characteristics, e.g. control-based or dataflow-oriented. However, this heterogeneity of processes poses a challenge for the consistency analysis of process networks. This research proposes a lightweight method for analyzing the consistency of such networks. The method employs interface automata as a bridge between the architectural model and heterogeneous components representing concrete models of processes. Utilising interface automata, consistency is determined by a series of small tasks at both the architecture level and the component level. This separation of concerns simplifies the handling of heterogeneous components and alleviates the potential state space explosion problem when analyzing large systems.
There have been a number of proposals for the integration of object-oriented capabilities into the Petri Net formalism. These proposals have demonstrated benefits for modelling, simulation and code generation. However, little has been said about analysis, particularly the use of state space methods, which are so prominent in Petri Net research and application. This talk will consider the impact of object oriented capabilities on state space analysis.
A software development methodology is defined that integrates software specification and validation efforts. The integration helps in achieving the twin goals of correct software with well-defined specifications that document it. The major focus of the paper is on dynamic lifecycle models. We indicate how language analysis of the problem description can be extended to derive not only a static class model for the system but also an initial dynamic lifecycle model. Consistency and completeness checks are provided which further drive the requirements elicitation. A case study is presented that clearly demonstrates the methodology.
Incremental development involves creating a new specification or implementation by modifying an existing one. This is a commonly used technique for handling complex systems in hardware and software engineering. In fact, incremental development is fundamental to object-orientation, the widely adopted approach to software engineering which uses the mechanism of inheritance.
Incremental development and object-orientation have been adopted for all phases of software engineering, from analysis to design and implementation. In the domain of concurrent systems, some researchers constrain incremental development by proposing requirements that must hold between the original and incrementally modified components. Such proposals are commonly based on a process algebra correctness relation, or require that a bisimulation relation hold between the original and modified components.
In Part I of this thesis we provide background on constraining incremental change and survey several existing proposals. We identify a number of problems typical of these proposals which commonly limit their practical use. We then present Incremental Coloured Petri Net Modelling which is aimed at addressing these problems. The main contribution of this part of the thesis is the identification of these problems and the assessment of the practical applicability of Incremental Coloured Petri Net Modelling. This assessment is made by examining several case studies published in the literature.
One of the primary benefits of using a formal method such as Coloured Petri Nets (CPNs) is its support for formal reasoning. State space analysis is a popular formal reasoning technique, but it is subject to state space explosion, where its application to real world models leads to unmanageably large state spaces.
In Part II of this thesis we first review existing approaches for alleviating the state space explosion problem. The main contribution of Part II is a new approach, which we call Incremental Analysis. Incremental Analysis involves algorithms which take advantage of Incremental CPN Modelling in attempting to alleviate the state space explosion problem. The thesis considers the implementation issues for these algorithms, identifies the situations under which they can be expected to lead to performance improvement, and presents case studies which demonstrate the value of the technique.
State space analysis is a popular formal reasoning technique. However, it is subject to the crippling problem of state space explosion, where its application to real world models leads to unmanageably large state spaces. In this paper we present algorithms which attempt to alleviate the state space explosion problem by taking advantage of the common practice of incremental development, i.e. where the designer starts with an abstract model of the system and progressively refines it. The performance of the incremental algorithm is compared to that of the standard algorithm for some case studies, and situations under which the performance improvement can be expected are identified.
This paper informally introduces Object Petri Nets (OPNs) with a number of examples. OPNs support a thorough integration of object-oriented concepts into Petri Nets, including inheritance and the associated polymorphism and dynamic binding. They have a single class hierarchy which includes both token types and subnet types, thereby allowing multiple levels of activity in the net. The paper discusses some theoretical issues pertinent to the analysis of OPNs, and compares the provisions of OPNs with those of other Concurrent Object-Oriented Programming Languages.The paper then considers a case study of using OPNs to model a cooperative editor for hierarchical diagrams. This extended example demonstrates the applicability of OPNs to the modelling of non-trivial concurrent systems. The methodology for deriving a Petri Net model is to adapt an object-oriented design methodology: the Object Model is prepared in RumbaughÕs OMT notation; the Dynamic Model is then prepared in the form of lifecycles, following the Shlaer-Mellor methodology; and finally these models are mapped into an OPN model. This approach has the advantage of guiding the development with well-accepted methodologies, and demonstrates the generality and flexibility of the OPN formalism.
An earlier paper considered appropriate properties for abstract net components (or nodes) in the Coloured Petri Net formalism. This paper augments that earlier work in three main areas Ñ it proposes general canonical forms for such node refinements, it identifies two other forms of refinement which will be used in concert with node refinement, and it considers the compositionality of these refinements. All of them maintain behavioural compatibility between refined and abstract nets, which is captured by the notion of a system morphism.
The rules for inheritance of classes with respect to data and function members are well defined. For example, the proposals for programming by contract in Eiffel ensure additional consistency between superclasses and subclasses. In object-oriented design, it is common to capture the behaviour of classes with lifecycles which are expressed in the form of finite state machines. In this context, there are very few proposals for what constitutes consistency between superclasses and subclasses.This paper presents proposals for consistency between superclasses and subclasses in the context of the Petri Net formalism, which is a form of finite state machine with explicit provisions for concurrency. The paper cites the applicability of these proposals in the context of network protocols, and argues for a similar applicability in the context of object lifecycles.
The object-oriented specification of concurrent and distributed systems has tended to emphasise the aspect of substitutability at the expense of code reuse. A variety of constraints has been imposed in order to guarantee substitutability in one form or another. This paper argues that the incremental development of software specifications needs to consider substitutability in the context of code reuse. Further, the common approach of starting with an abstract specification and then progressively refining it (in some general way) means that many existing substitutability constraints are too strong. In the context of Coloured Petri Nets, we advocate the use of three specific forms of refinement - type refinement, subnet refinement, and node refinement. These have weaker demands for substitutability, namely that every (complete) refined behaviour has a corresponding abstract behaviour, but not necessarily vice versa. An examination of case studies in the literature suggests that this approach is applicable in practice.
This paper examines how object-oriented extensions to the Petri Net formalism provide flexible structuring primitives which can aid the modelling of network protocols. A key benefit is the support for incremental modelling. As a result, a protocol can be modelled as a collection of services, each of which can be expressed as the enhancement of a basic service, in which case, both the structure of the basic service and the nature of the enhancement can be clearly identified. More importantly, the evolution of a protocol through a sequence of standards can be expressed by progressive refinements. The object-oriented extensions are captured in the formalism of Object Petri Nets, with a textual language form referred to as LOOPN++, both of which are introduced in this paper. The incremental modelling capabilities and their benefits are demonstrated for the Z39.50 Protocol for Information Retrieval.
An earlier paper considered the appropriate properties for abstract net components in the Coloured Petri Net formalism. This paper extends that earlier work in refining some definitions and in proving compositionality properties. The primary result is that the composition of abstractions, under certain conditions, is also an abstraction. The practical use of abstraction is indicated by a solution to the sliding window protocol, where the abstract behaviour captures important properties of the protocol.
This paper presents three forms of incremental change or refinement which are considered appropriate for Coloured Petri Nets. The intention is to recommend forms which are appropriate to Petri Nets and not primarily driven by the desire to emulate object-oriented programming languages. Nevertheless, the proposals are compared with others in the literature Ñ with object-oriented programming languages, with practical case studies of the application of formal methods, and with other object-oriented Petri Net formalisms.
This technical report describes some incremental reachability algorithms for Petri nets. Such algorithms are designed to take advantage of incremental changes to a formal model to improve the efficiency of the reachable state space generation. This report presents incremental changes that are considered appropriate for Coloured Petri Nets and then presents and discusses some algorithms that take advantage of such incremental. It is intended that this report will act as a reference for the implementation of the incremental algorithms.
Object Data Management Systems (ODMSs) are a relatively new type of information management tool. They have emerged to provide support for the management of complex data in data-intensive applications like Computer-Aided Design and Computer-Aided Software Engineering. We develop an interface to an ODMS through the LOOPN++ programming language. LOOPN++ is based on Petri Nets and object-orientation, and a useful tool for dynamically controlling data access.
This paper considers the appropriate properties for abstract net components in the Coloured Petri Net formalism. In doing so, it attempts to maintain the duality between places and transitions which is so foundational to Petri Net theory. It also defines what it means to execute the net at an abstract level.
This paper proposes the generation of Java applets from specifications given in an extended Petri Net formalism. The anticipated advantages of this approach are to gain a greater confidence in the correctness of the final product, and to harness the capabilities of Java in a consistent framework. The emphasis of this paper is on the generation of the Java code from the Petri Net specification, on the assessment of both Java and C++ as suitable targets for this translation, and on the suitability of this extended form of Petri Nets as a host for various extensions to Java.
This paper seeks to present a more elegant and general definition of Object Petri Nets than previously. It is more general since it supports transition fusion as well as place fusion. It is more elegant because it captures all the notions of place substitution, transition substitution, place fusion, and transition fusion under the single notion of binding. This is achieved by explicitly supporting names in the formalism, in line with the ¹-calculus which recognises that names are pervasive and should be explicitly included in a formalism in order to model object mobility. The definition in this paper is also more consistent in its use of polymorphism and embodies a more obvious duality between states and changes of state. Object Petri Nets represent a complete integration of object-oriented concepts into Petri Nets. They have a single class hierarchy which includes both token types and subnet types, and which readily supports modelling systems with multiple levels of activity. Interaction between subnets can be synchronous or asynchronous depending on whether the subnet is defined as a super place or a super transition. While not presented in this paper, Object Petri Nets can be transformed into behaviourally equivalent Coloured Petri Nets, thus providing a basis for adapting existing analysis techniques.
This paper presents a case study on the use of Object Petri Nets. The case study is that of a cooperative editor for hierarchical diagrams. The methodology for deriving the Petri Net model is to follow an object-oriented design methodology: first we prepare the Object Model in the OMT notation of Rumbaugh; then we prepare the Dynamic Model in the form of lifecycles, following the Shlaer-Mellor methodology; and finally we map these models into an Object Petri Net model. This approach has the advantage of guiding the development with well-accepted methodologies, but has the disadvantage of overlooking valid Petri Net solutions to the problem. As a result of this exercise, some loose ends in the Shlaer-Mellor methodology are identified and resolved, and a modification to the semantics of OPN super transitions is proposed. However, one overriding conclusion of this paper is that Object Petri Nets are suitable as a target formalism in such an object-oriented design methodology.
This paper presents the concept of reflection, where a program modifies its own interpretation. A number of applications of reflection are examined and it becomes apparent that the technique is particularly applicable to the implementation of object-oriented languages. The paper then considers how the technique can be applied to the implementation of Object Petri Nets (OPNs), a formalism for modelling concurrent, object-oriented systems. It turns out that reflection provides a simple and efficient implementation scheme for the compositionality constructs of OPNs. Further, it allows flexible scheduling strategies to be employed in the simulation of OPNs.
The programming language Java has become and extremely popular language; many people are writing concurrent systems using Java. The design and implementation of concurrent Java programs is significantly more complex than sequential programs and the use formal method is seen as extremely beneficial for the design and implementation of such systems. The Petri net formalism [Petri 1962] can be used for the design, specification, simulation, verification, validation and implementation of concurrent systems. Object Petri Nets (OPNs) represent a complete integration of Petri nets and object-orientated concepts and therefore provide the many benefits of object-orientation to the Petri net formalism. This thesis presents an examination of concurrent object-oriented languages with a particular emphasis on object-oriented Petri net languages; a review of Java is also provided. The many benefits of OPNs are seen as an ideal method for the design, specification and implementation of concurrent Java programs. To allow OPNs to be used to for the implementation of concurrent Java programs, the integration of OPNs and Java was required. This has been accomplished by the development of LOOPN++ (Language for Object-Oriented Petri Nets) to Java compiler. This compiler was realised by the development of a new back-end for an existing LOOPN++ to C++ compiler. The development of a LOOPN++ to Java compiler has also meant that the simulation of a LOOPN++ Petri net was improved.
This technical report describes a language and simulator for specifying systems in terms of Object Petri Nets. These petri nets are a variant of Coloured Petri Nets with the inclusion of simulated time and a complete integration of object-oriented features. These features serve to break away from the traditional approach of viewing the data as essentially passive and the petri net as a global control structure. These features also encourage the convenient modularisation of complex specifications and allow for the possibility of model reuse.
This technical report considers the appropriate properties for abstract net components in the Coloured Petri Net formalism. In doing so, it attempts to maintain the duality between places and transitions which is so foundational to Petri Net theory. It also defines what it means to execute the net at an abstract level.
This paper seeks to establish within a formal framework how Coloured Petri Nets can be enhanced to produce Object Petri Nets. It does so by defining a number of intermediate Petri Net formalisms and identifying the features introduced at each step of the development. Object Petri Nets support a complete integration of object-oriented concepts into Petri Nets, including inheritance and the associated polymorphism and dynamic binding. In particular, Object Petri Nets have a single class hierarchy which includes both token types and subnet types. Interaction between subnets can be either synchronous or asynchronous depending on whether the subnet is defined as a super place or a super transition. The single class hierarchy readily supports multiple levels of activity in the net and the generation and removal of tokens has been defined so that all subcomponents are simultaneously generated or removed, thus simplifying memory management. Despite this descriptive power, Object Petri Nets can be transformed into behaviourally equivalent Coloured Petri Nets, thus providing a basis for adapting existing analysis techniques.
This paper presents Object Petri Nets (OPNs), a formal system which integrates object-oriented structuring into the Petri Net formalism. The paper considers some proposed relationships between a class and its superclass, including variations on signature and behaviour compatibility. These proposals are evaluated in the context of a number of simple case studies, which serve to show that many suggested solutions do not work in practice. It is suggested that this critique applies equally well to other concurrent object-oriented languages.
This paper examines how object-oriented extensions to the Petri Net formalism can address a number of issues in the modelling of network protocols. The object-oriented extensions lead to the formalism of Object Petri Nets, with a textual language form referred to as LOOPN++. The paper considers practical examples for which clean, well-structured models can be created because of the support for modularity, inheritance, polymorphism, genericity, and mobile objects.
This paper informally introduces Object Petri Nets (OPNs) with a number of examples and discusses how this kind of Petri Net addresses a number of issues pertinent to Concurrent Object-Oriented Programming Languages. OPNs support a thorough integration of object-oriented concepts into Petri Nets, including inheritance and the associated polymorphism and dynamic binding. They have a single class hierarchy which includes both token types and subnet types, thereby allowing multiple levels of activity in the net. Yet OPNs retain the important property of being able to be transformed into behaviourally equivalent Coloured Petri Nets (CPNs), which can provide a foundation for adapting existing analysis techniques such as invariant analysis.
This paper proposes Object Petri Nets as an appropriate semantic foundation on which to build an open software engineering environment. The well-established graphical notation for Petri Nets can be readily adapted to the diagrams produced by object-oriented analysis and design methods, as is demonstrated for the work products of the Shlaer-Mellor methodology. The semantics of Object Petri Nets provides the basis for prototyping and code generation. Furthermore, the current implementation style for LOOPN++, a textual language for Object Petri Nets, supports the smooth integration of other software components such as object data stores and networking interfaces.
This paper proposes an approach to arc extensions in CP-nets which is claimed to be both general and systematic. It is general because the enabling rules cater for true concurrency as well as an interleaving semantics and because it encompasses the other proposals for arc extensions that have been made recently in the Petri Net literature, often in the context of the requirements of specific application domains. It is systematic because it proposes a set of fundamental arcs in the context of a general complementary place construction and then considers how these arcs can be combined in arbitrary ways. Because of the utility of some of these compound arcs and the minimal overhead in implementing them, it is argued that CP-net tools should provide explicit support for them.
In recent years, there has been significant interest in combining the benefits of object-oriented structuring techniques with the petri net formalism which has proved beneficial in the modelling and simulation of concurrent systems. This paper presents a more extensive application of object-oriented ideas to Coloured Petri Nets, in that it breaks away from the traditional approach of viewing the data as essentially passive and the petri net as a global control structure. The paper presents a textual language for specifying object-oriented petri nets which is convenient for modelling complex concurrent systems. The underlying formalism provides the basis for transforming object-oriented nets into Coloured Petri Net models where traditional analysis techniques can be applied.
There have been significant recent developments in high level specification schemes for modelling information systems using formalisms based on petri nets. In particular, the application of object-based design principles have produced high level petri nets which can be used to model large complex systems. This paper discusses a new language and modelling scheme, known as LOOPN++, which fully integrates the concepts of object-oriented language design and model building into a coloured petri net system. The completeness and clarity of LOOPN++ are discussed with respect to its use in the dynamic modelling of information systems.
An examination of the Z39.50 protocol in its context is made, and a methodology for expressing it in Petri nets is proposed and implemented. The resulting place/transition nets are expressed in LOOPN modules and source code. Advantages and difficulties of the use of this particular form of expression are noted, and recommendations for further analysis and work in this area are made.
The continuing development of LOOPN, a language for object-oriented Petri nets, has resulted in Xloopn, an X-Windows graphical screen editor. The extension of Xloopn to allow communication with other Petri net tools is considered an important step. The integration of such a mechanism into the interface requires careful design. An examination of existing Petri net package interfaces has been undertaken to provide the necessary background to design the simulator tool interface elements. The mechanism to allow simulation of Petri nets created in Xloopn has been realised and has been integrated smoothly with the current interface.
This paper demonstrates how Object Petri Nets can be developed from the definition of Coloured Petri Nets. It does so by defining a number of intermediate petri net formalisms and identifying the features introduced at each step of the development. Object Petri Nets support a complete integration of object-oriented concepts into petri nets, including inheritance and the associated polymorphism and dynamic binding. In particular, Object Petri Nets have a single class hierarchy which includes both token types and subnet types. Interaction between subnets can be either synchronous or asynchronous depending on whether the subnet is defined as a super place or a super transition. The single class hierarchy readily supports multiple levels of activity in the net and the generation and removal of tokens has been defined so that all subcomponents are simultaneously generated or removed. Despite this descriptive power, Object Petri Nets can be transformed into behaviourally equivalent Coloured Petri Nets, so that many existing analysis techniques can be readily applied.
In recent years, there has been significant interest in combining the benefits of object-oriented structuring techniques with the petri net formalism which has proved beneficial in the modelling and simulation of concurrent systems. This paper presents a more extensive application of object-oriented ideas to Coloured Petri Nets, in that it breaks away from the traditional approach of viewing the data as essentially passive and the petri net as a global control structure. The paper presents a textual language for specifying object-oriented petri nets which is convenient for modelling complex concurrent systems. The underlying formalism provides the basis for transforming object-oriented nets into Coloured Petri Net models where traditional analysis techniques can be applied.
In recent years, there has been significant interest in combining the benefits of object-oriented structuring techniques with the petri net formalism which has proved beneficial in modelling concurrent systems. This paper presents a more extensive application of object-oriented ideas to Coloured Petri Nets, in that it breaks away from the traditional approach of viewing the data as essentially passive and the petri net as a global control structure. The resultant class of petri nets are called Object Petri Nets. These are formally defined in the paper, are illustrated by an example, and are proven to be behaviourally equivalent to Coloured Petri Nets, thus providing the basis for applying traditional analysis techniques.
Object-oriented development systems traditionally have the benefits of encouraging well-modularised code with clean interfaces, and being able to provide reusable modules. Frequently, the penalty for such environments is the size and possibly speed of generated code. This paper presents a case study of designing an electronic door controller system which is to run on a central PC and distributed door control units which consist of tightly constrained Z80 processors.The initial prototype was developed in LOOPN, a language and simulator for specifying systems in terms of coloured timed petri nets. This prototype was primarily implemented to isolate protocol errors and possible timing problems. However, the code of the prototype could also be adapted to produce the running system in the door controller units. This paper briefly describes LOOPN and considers its application to the modelling of a door control system and its associated network protocol. It also indicates how the target code could be adapted to produce the run-time system.
LOOPN is a language and simulator for specifying systems in terms of coloured timed petri nets. It includes object-oriented features such as subtyping, inheritance and polymorphism which allow for the convenient modularisation of complex specifications. This paper examines the issue of modular correctness, and the extent to which the traditional invariant analysis of petri nets is applicable. In doing so, it considers the proposals for calculating modular place flows proposed by Christensen and Petrucci. It also discusses the limitations of invariant analysis as identified by Reisig. The paper illustrates these ideas with the standard producer-consumer problem and a sliding window protocol.
LOOPN is a language and simulator for specifying systems in terms of coloured timed petri nets. It includes object-oriented features such as sub-typing, inheritance and polymorphism which allow for the convenient modularisation of complex specificaÐtions. LOOPN has been used to specify, implement and test discrete event simulation systems, particularly in the areas of distributed database and associated communication protocols. The object-oriented structure of LOOPN and its polymorphism make it well suited to both the design process and to the specification of complex systems which may be modelled using a multiple layered hierarchy (Lakos and Keen 1991). This paper examines a range of object-oriented development methodologies which are applicable to the design and analysis of discrete event simulation models, especially to the development of such models using object-oriented petri nets as the target language.
This paper proposes an approach to arc extensions in CP-nets which is claimed to be both general and systematic. It is general because the enabling rules cater for true concurrency as well as an interleaving semantics and because it encompasses the other proposals for arc extensions that have been made recently in the Petri Net literature, often in the context of the requirements of specific application domains. It is systematic because it proposes a set of fundamental arcs in the context of a general complementary place construction and then considers how these arcs can be combined in arbitrary ways. Because of the utility of some of these compound arcs and the minimal overhead in implementing them, it is argued that CP-net tools should provide explicit support for them.
Hierarchical Coloured Petri Nets provide a powerful technique for modelling concurrent systems. The colouring of tokens avoids the need for unnecessarily duplicating the control structure of the net, as is the case for the simpler place/transition nets. The decomposition of complex nets is further encouraged by the provision of hierarchy constructs, whereby a subnet can be isolated as a separate page. It is common to find substitution transitions and place fusion sets implemented as the hierarchy constructs of coloured petri net tools. This paper examines the provision of substitution places and considers why this construct has not been more popular. It suggests an improved semantics for the construct to that originally proposed; it proposes a desirable extension; and it considers the contexts where this sort of construct would be most desirable.
Place summary functions have been provided in LOOPN, a Language for Object-Oriented Petri Nets. A place summary function computes some value from the multiset of tokens which is the current place marking. The construct in LOOPN has proved to be invaluable in the modelling of complex systems, because it encourages good encapsulation and clean interfaces between subnets. This report provides a formal definition of place summary functions in the context of Coloured Petri Nets and proves that nets extended with this construct are behaviourally equivalent to standard coloured petri nets. This result will, in due course, form part of the proof that LOOPN nets are behaviourally equivalent to standard coloured petri nets.
Petri nets have been used to model and analyse distributed systems. High-level nets such as coloured nets and object-oriented nets increase the descriptive power by allowing the tokens which flow through the net to be associated with arbitrary data values. Algorithms have been specified for the distributed simulation of simple petri nets on a set of transputers. This paper considers the extension of these algorithms for high-level nets and discusses the problems involved in achieving a fair implementation.
This technical report documents the choices made in implementing LOOPN, a language and simulator for specifying systems in terms of object-oriented timed petri nets. The petri nets supported are a variant of coloured petri nets with the inclusion of simulated time and object-oriented features such as subtyping, inheritance and polymorphism, which encourage the convenient modularisation of complex specifications.
This technical report describes a language and simulator for specifying systems in terms of object-oriented timed petri nets. The petri nets supported are a variant of coloured petri nets with the inclusion of simulated time and object-oriented features such as subtyping, inheritance and polymorphism, which encourage the convenient modularisation of complex specifications.
LOOPN is a language and simulator for specifying systems in terms of coloured timed petri nets. It includes object-oriented features such as subtyping, inheritance and polymorphism which allow for the convenient modularisation of complex specifications. This paper briefly describes LOOPN and considers its application to the modelling of layered network protocols.
LOOPN is a language and simulator for specifying systems in terms of coloured timed petri nets. It includes object-oriented features such as subtyping, inheritance and polymorphism which allow for the convenient modularisation of complex specifications. This paper describes LOOPN and the experience that has been gained in its use both for discrete event simulation purposes and more specifically for modelling network protocols.
LOOPN is a language and simulator for specifying systems in terms of coloured timed petri nets. It includes object-oriented features such as subtyping, inheritance and polymorphism which allow for the convenient modularisation of complex specifications. This paper describes the evolution of LOOPN and the experience that has been gained in its use both for discrete event simulation purposes and more specifically for modelling network protocols.
Date created: 14 April 1999 Last modified: 20 January 2004 Copyright © 1996, Charles Lakos Maintained by: Charles Lakos Charles.Lakos@adelaide.edu.au