Wyniki wyszukiwania - BazTech

1

Generalizing the Compositions of Petri Nets Modules

Marechal A., Buchs D.

Fundamenta Informaticae

|

2015

|

Vol. 137, nr 1

87--116

EN

Modularity is a mandatory principle to apply Petri nets to real world-sized systems. Modular extensions of Petri nets allow to create complex models by combining smaller entities. They facilitate the modeling and verification of large systems by applying a divide and conquer approach and promoting reuse. Modularity includes a wide range of notions such as encapsulation, hierarchy and instantiation. Over the years, Petri nets have been extended to include these mechanisms in many different ways. The heterogeneity of such extensions and their definitions makes it difficult to reason about their common features at a general level. We propose in this article an approach to standardize the semantics of modular Petri nets formalisms, with the objective of gathering even the most complex modular features from the literature. This is achieved with a new Petri nets formalism, called the LLAMAS Language for Advanced Modular Algebraic Nets (LLAMAS). We focus principally on the composition mechanism of LLAMAS, while introducing the rest of the language with an example. The composition mechanism is introduced both informally and with formal definitions. Our approach has two positive outcomes. First, the definition of new formalisms is facilitated, by providing common ground for the definition of their semantics. Second, it is possible to reason at a general level on the most advanced verification techniques, such as the recent advances in the domain of decision diagrams.

2

Synchronous and Asynchronous Communications in Composable Parameterized High-Level Petri Nets

Devillers R., Klaudel H.

Fundamenta Informaticae

|

2005

|

Vol. 66, nr 3

221--257

EN

In the domain of parameterized composable high-level Petri nets (M-nets), we shall combine the refinement, the synchronization and the asynchronous link operations in a unified and general setup, while keeping the expected properties of those operations. In particular, the various high-level net operations are consistent through unfolding with their low-level counterparts, and the usual commutativity and idempotency properties are fulfilled at the syntactic level up to structural equivalences.

3

Petri nets and resource bisimulation

Bashkin V.A., Lomazova I.A.

Fundamenta Informaticae

|

2003

|

Vol. 55, nr 2

101-114

EN

Resources are defined as submultisets of Petri net markings. Two resources are called similar if replacing one of them by another in any marking doesn't change the Petri net's behavior. We define the relations of resource similarity and resource bisimulation and show that they are finitely based. In this paper the resource bisimulation is studied for different classes of Petri nets: ordinary Petri nets, high-level Petri nets and nested Petri nets - Petri nets with Petri nets as tokens.

4

Time extensions of Petri nets for modelling and verification of hard real-time systems

Samolej S., Szmuc T.

Computer Science

|

2002

|

Vol. 4

55-76

EN

The main aim of the paper is a presentation of time extensions of Petri nets appropriate for modelling and analysis of hard real-time systems. It is assumed, that the extensions must provide a model of time flow, an ability to force a transition to fire within a stated timing constraint (the so-called the strong firing rule), and timing constraints represented by intervaIs. The presented survey includes extensions of classical Place/Transition Petri nets, as welI as the ones applied to high-level Petri nets. An expressiveness of each time extension is illustrated using simple hard real-time system. The paper includes also a brief description of analysis and verification methods related to the extensions, and a survey of software tooIs supporting modelling and analysis of the considered Petri nets.

PL

Głównym celem pracy jest prezentacja rozszerzeń czasowych sieci Petriego pod kątem przydatności do modelowania i analizy systemów czasu rzeczywistego o twardych wymaganiach losowych. Zakłada się, że rozważane rozszerzenia winny spełniać następujące warunki: modelowania upływu czasu, forsowania odpalenia przejścia w określonych warunkach czasowych (tzw. silna reguła odpalania), przedziałowej reprezentacji ograniczeń czasowych. Przegląd dotyczy zarówno klasycznych sieci miejsc i przejść, jak również sieci Petriego wyższego poziomu. Siła ekspresji poszczególnych rozszerzeń jest ilustrowana na wspólnym przykładzie systemu o twardych wymaganiach czasowych. Artykuł zawiera również krótki opis metod analizy i weryfikacji ograniczeń czasowych oraz przegląd systemów wspomagających modelowanie i analizę rozważanych sieci Petriego.

5

Generalised composition operations for high-level Petri nets

Best E., Lavrov A.

Fundamenta Informaticae

|

1999

|

Vol. 40, Nr 2,3

125-163

EN

We propose generic schemes for basic composition operations (sequential composition, choice, iteration, and refinement) for high-level Petri nets. They tolerate liberal combinations of place types (equal, disjoint, intersecting) and, owing to a parameterised scheme of type construction, allow for weak and strong versions of compositions. Properties such as associativity, commutativity, and coherence with respect to unfolding, are preserved.