scholarly journals Modelling and Analysis of Distributed Program Execution in BETA Using Coloured Petri Nets

1997 ◽  
Vol 26 (513) ◽  
Author(s):  
Jens Bæk Jørgensen ◽  
Kjeld Høyer Mortensen
Keyword(s):  
Petri Nets ◽  
Case Studies ◽  
Object Oriented ◽  
Coloured Petri Nets ◽  
Program Execution ◽  
Shared Resources ◽  
Computer Tools ◽  
Remote Object ◽  
Critical Regions

<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>

scholarly journals Teaching Coloured Petri Nets - a Gentle Introduction to Formal Methods in a Distributed Systems Course

1997 ◽  
Vol 26 (520) ◽  
Author(s):  
Søren Christensen ◽  
Kjeld Høyer Mortensen
Keyword(s):  
Distributed Systems ◽  
Petri Nets ◽  
Formal Methods ◽  
Case Studies ◽  
Formal Method ◽  
Object Oriented ◽  
Coloured Petri Nets ◽  
Basic Concepts

<p>This paper is about the two compulsory project assignments set to the students in an undergraduate course on distributed systems. In the first assignment the students design and validate a non-trivial layered protocol by means of Coloured Petri Nets, and in the second they implement the designed protocol in an object-oriented language. From the two assignments the students experience that Coloured Petri Nets, as a formal method, are useful for designing and analysing distributed systems. In the course students are introduced to basic concepts and techniques for distributed systems, and it is explained that such systems are often too complex to manage without using formal methods. In this paper we also report on our experience with teaching the course and describe the didactic methods applied. Based on the obtained experience we conclude that the combination of distributed systems and Coloured Petri Nets is fruitful --- the two areas complement each other. Although our experiences origin in Coloured Petri Nets, we believe that many of our observations hold for other formal methods as well.</p><p><strong>Topics.</strong> Education issues related to nets; Coloured Petri Nets; distributed systems; experience with using nets,case studies; applications of nets to protocols.</p>

scholarly journals On Modeling and Simulation of Resource Allocation Policies in Cloud Computing Using Colored Petri Nets

2020 ◽  
Vol 10 (16) ◽  
pp. 5644 ◽  
Author(s):  
Stavros Souravlas ◽  
Stefanos Katsavounis ◽  
Sofia Anastasiadou
Keyword(s):  
Resource Allocation ◽  
Petri Nets ◽  
Petri Net ◽  
Object Oriented ◽  
Colored Petri Nets ◽  
Allocation Scheme ◽  
Shared Resources ◽  
Basic Characteristics ◽  
Resource Allocation Scheme ◽  
Maximum Utilization

The Petri net (PN) formalism is a suitable tool for modeling parallel systems due to its basic characteristics, such as synchronization. The extension of PN, the Colored Petri Nets (CPN) allows the incorporation of more details of the real system into the model (for example, contention for shared resources). The CPNs have been widely used in a variety of fields to produce suitable models. One of their biggest strengths is that their overall philosophy is quite similar to the philosophy of the object-oriented paradigm. In this regard, the CPN models can be used to implement simulators in a rather straightforward way. In this paper, the CPN framework is employed to implement a new resource allocation simulator, which is used to verify the performance of our previous work, where we proposed a fair resource allocation scheme with flow control and maximum utilization of the system’s resources.

scholarly journals Analysing Bang & Olufsen's BeoLink Audio/Video System Using Coloured Petri Nets

1997 ◽  
Vol 26 (514) ◽  
Author(s):  
Søren Christensen ◽  
Jens Bæk Jørgensen
Keyword(s):  
Petri Nets ◽  
Living Room ◽  
Coloured Petri Nets ◽  
Main Experiment ◽  
Validation And Verification ◽  
State Spaces ◽  
Computer Tools ◽  
Graphical Feedback ◽  
Future Revision ◽  
Audio Video

<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>

Sign in / Sign up

Export Citation Format

Share Document