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>

scholarly journals Design/CPN - A Computer Tool for Coloured Petri Nets

1997 ◽  
Vol 26 (511) ◽  
Author(s):  
Søren Christensen ◽  
Jens Bæk Jørgensen ◽  
Lars Michael Kristensen
Keyword(s):  
Petri Nets ◽  
Industrial Application ◽  
World Wide ◽  
Coloured Petri Nets ◽  
Computer Tool ◽  
Design Validation ◽  
Validation And Verification ◽  
State Space Analysis ◽  
Video Systems ◽  
Audio Video

In this paper, we describe the computer tool Design/CPN supporting editing, simulation, and state space analysis of Coloured Petri Nets. So far, approximately 40 man-years have been invested in the development of Design/CPN. It is used world-wide by more than 200 companies and research institutions. For the presentation, we draw from the experiences gained in recent industrial application using Coloured Petri Nets in the design, validation, and verification of communication protocols for audio/video systems.

scholarly journals Model Checking Coloured Petri Nets - Exploiting Strongly Connected Components

1997 ◽  
Vol 26 (519) ◽  
Author(s):  
Allan Cheng ◽  
Søren Christensen ◽  
Kjeld Høyer Mortensen
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
The State ◽  
Connected Components ◽  
Coloured Petri Nets ◽  
Transition Systems ◽  
Strongly Connected Components ◽  
State Spaces ◽  
Labelled Transition Systems ◽  
Strongly Connected

In this paper we present a CTL-like logic which is interpreted over the state spaces of Coloured Petri Nets. The logic has been designed to express properties of both state and transition information. This is possible because the state spaces are labelled transition systems. We compare the expressiveness of our logic with CTL's. Then, we present a model checking algorithm which for efficiency reasons utilises strongly connected components and formula reduction rules. We present empirical results for non-trivial examples and compare the performance of our algorithm with that of Clarke, Emerson, and Sistla.

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>

Validation and Verification of Software Systems Using Virtual Reality and Coloured Petri Nets

2007 ◽  
pp. 28-54
Author(s):  
Hyggo Almeida ◽  
Leandro Silva ◽  
Glauber Ferreira ◽  
Emerson Loureiro ◽  
Angelo Perkusich
Keyword(s):  
Virtual Reality ◽  
Embedded System ◽  
Petri Nets ◽  
Formal Methods ◽  
Software Tool ◽  
Software Systems ◽  
Coloured Petri Nets ◽  
Validation And Verification ◽  
Verification Techniques

Validation and verification techniques have been identified as suitable mechanisms to determine if the software meets the needs of the user and to verify if the software works correctly. However, the existing verification techniques do not support friendly visualization. Also, validation techniques with friendly visualization mechanisms do not allow the verification of the system’s correctness. In this chapter, we present a method for the validation and verification of software systems through the integration of formal methods and virtual reality. Furthermore, a software tool associated with such a method is also described along with an embedded system case study.

scholarly journals Computer Aided Verification of Lamport's Fast Mutual Exclusion Algorithm - Using Coloured Petri Nets and Occurrence Graphs with Symmetries

1997 ◽  
Vol 26 (512) ◽  
Author(s):  
Jens Bæk Jørgensen ◽  
Lars Michael Kristensen
Keyword(s):  
Distributed Systems ◽  
Petri Nets ◽  
Mutual Exclusion ◽  
Condensed State ◽  
Coloured Petri Nets ◽  
Computer Tool ◽  
State Spaces ◽  
Index Terms ◽  
High Level ◽  
Mutual Exclusion Algorithm

<p>In this paper, we present a new computer tool for verification of distributed systems. As an example, we establish the correctness of Lamport's Fast Mutual Exclusion Algorithm. The tool implements the method of occurrence graphs with symmetries (OS-graphs) for Coloured Petri Nets(CP-nets). The basic idea in the approach is to exploit the symmetries inherent in many distributed systems to construct a condensed state space. We demonstrate a signigicant increase in the number of states which can be analysed. The paper is to a large extent self-contained and does not assume any prior knowledge of CP-nets (or any other kinds of Petri Nets) or OS-graphs. CP-nets and OS-graphs are not our invention. Our contribution is development of the tool and verification of the example.</p><p><strong>Index Terms:</strong> Modelling and Analysis of Distributed Systems, Formal Verification, Coloured Petri Nets, High-Level Petri Nets, Occurrence Graphs, State Spaces, Symmetries, Mutual Exclusion.</p>

scholarly journals Construction of Occurrence Graphs with Permutation Symmetries Aided by the Backtrack Method

2002 ◽  
Vol 26 (516) ◽  
Author(s):  
Jens Bæk Jørgensen
Keyword(s):  
Group Theory ◽  
Petri Nets ◽  
Performance Measures ◽  
New Method ◽  
Coloured Petri Nets ◽  
State Spaces ◽  
Experimental Performance ◽  
Speed Up ◽  
Backtrack Algorithm ◽  
Reduced State

<p>This paper recalls the concept of occurrence graphs with permuta- tion symmetries (OS-graphs) for Coloured Petri Nets. It is explained how so-called self-symmetries can help to speed up construction of OS- graphs. The contribution of the paper is to suggest a new method for calculation of self-symmetries, the Backtrack Method. The method is based on the so-called Backtrack Algorithm, which originates in com- putational group theory. The suggestion of the method is justified, both by identifying an important general complexity property and by obtaining encouraging experimental performance measures.</p><p><strong>Topics.</strong> Coloured Petri Nets, reduced state spaces, occurrence graphs with permutation symmetries, self-symmetries, computational group theory, backtrack searches.</p>

scholarly journals Coloured Petri Nets: A High Level Language for System Design and Analysis

1993 ◽  
Vol 19 (338) ◽  
Author(s):  
Kurt Jensen
Keyword(s):  
Petri Nets ◽  
Software Systems ◽  
Coloured Petri Nets ◽  
Human Beings ◽  
High Level Language ◽  
Design Specification ◽  
Computer Tools ◽  
Simulation Validation ◽  
Definition Of ◽  
High Level

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

Sign in / Sign up

Export Citation Format

Share Document