Computer Tools for Coloured Petri Nets

1992 ◽  
pp. 155-203 ◽  
Author(s):  
Kurt Jensen
1997 ◽  
Vol 26 (513) ◽  
Author(s):  
Jens Bæk Jørgensen ◽  
Kjeld Høyer Mortensen

<p>Recently, abstractions supporting distributed program execution in the object-oriented language BETA have been designed. A BETA object on one computer may invoke a remote object, i.e., an object hosted by another computer. In this project, the formalism of Coloured Petri Nets (CP-nets or CPN) is used to describe and analyse the protocol for remote object invocation. In the first place, we build a model in order to describe, understand, and improve the protocol. Remote object invocation in BETA is modelled on the level of threads (lightweight processes) with emphasis on the competition for access to critical regions and shared resources. Secondly, the model is analysed. It is formally proved that it has a set of desirable properties, e.g., absence of dead markings.</p><p><strong>Topics:</strong> Systemdesign and verfication using nets; higher-level nets models; computer tools for nets; experience with using nets, case studies; application of nets to protocols.</p>


1997 ◽  
Vol 26 (514) ◽  
Author(s):  
Søren Christensen ◽  
Jens Bæk Jørgensen

<p>Bang &amp; Olufsen A/S (B&amp;O) is a renowned manufacturer of audio and video products. Their BeoLink (BeoLink) system distributes sound and vision throughout a home via a network. In this way, e.g., while doing the cooking in the kitchen, a person can remotely select and listen to a track from a CD, loaded in the CD player situated in the living room. To resolve conflicts, synchronisation between various actions is needed, and is indeed taken care of by appropiate communication protocols.</p><p>The purpose of the project described in this paper vas to test Coloured Petri Nets (CP-nets or CPN) as a way to improve B&amp;O's methods for specification, validation, and verification of protocols. In the main experiment, an engineer from B&amp;O used the Desing/CPN tool to build a simulations with a familiar graphical feedback, and to formally verify crucial properties using occurrence graphs (also known as state spaces and reachability graphs/trees). The latter activity demonstrated the applicability of occurrence graphs for timed CP-nets. Moreover, CPN was used to examine important aspects of a possible future revision of Beo-Link, and to check compatibility between the new and the old version. Based on the experiments reported in this paper, CPN has been included in the set of methods for specification, validation, and verification of future protocols at B&amp;O.</p><p> </p><p><strong>Topics:</strong> System design oand verification using nets; higher-level net models; computer tools for nets; experience with using nets, case studies; application of nets to protocols and embedded systems.</p>


1993 ◽  
Vol 19 (338) ◽  
Author(s):  
Kurt Jensen

This paper describes how Coloured Petri Nets (CP-nets) have been developed - from being a promising theoretical model to being a full-fledged language for the design, specification, simulation, validation and implementation of large software systems (and other systems in which human beings and/or computers communicate by means of some more or less formal rules). First CP-nets are introduced by means of a small example and a formal definition of their structure and behaviour is presented. Then we describe how to extend CP-nets by a set of hierarchy constructs (allowing a hierarchical CP-net to consist of many different subnets, which are related to each other in a formal way). Next we describe how to analyse CP-nets, how to support them by various computer tools, and we also describe some typical applications. Finally, a number of future extensions are discussed (of the net model and the supporting software).


Author(s):  
Manuel Cheminod ◽  
Ivan Cibrario Bertolotti ◽  
Luca Durante ◽  
Adriano Valenzano

Sign in / Sign up

Export Citation Format

Share Document