Metody analýzy objektově orientovaných Petriho sítí

Analysis Methods of Object Oriented Petri Nets

dizertace

čeština

Objektově orientované Petriho sítě (OOPNs) jsou formalizmem, který je vhodný pro modelování, prototypování a formální analýzu a verifikaci paralelních (angl. concurrent) systémů. OOPNs spojují koncepty Petriho sítí (modelování kauzality, nedeterminizmu a paralelizmu v diskrétních systémech) s objektovou orientací (zapouzdření, dědičnost, polymorfizmus). Zavedení tříd a objektů do Petriho sítí umožňuje (z praktického hlediska velice užitečné) snadné a přirozené vytváření rozsáhlých a přesto přehledných modelů. Formální analýza a verifikace OOPN modelů je možná, protože OOPNs jsou formálně definovány, ale je poměrně složitá, protože OOPNs jsou bohatým modelovacím formalizmem.

Tato práce rozvíjí dvě metody formální analýzy OOPN modelů. První zkoumanou metodou je typová analýza OOPN modelů, jejímž cílem je určit typy značek, které se při evoluci mohou dostat do jednotlivých míst modelu. V této práci jsou nejdříve popsány základní principy, na nichž je typová analýza OOPNs založena, a poté jsou navrženy dva algoritmy pro typovou analýzu - tzv. statická a dynamická typová analýza. Tyto algoritmy různým způsobem přistupují k dynamickému charakteru OOPNs. Statická typová analýza představuje méně přesnou ale rychlejší a jednodušší možnost, zatímco dynamická typová analýza je potenciálně přesnější ale pomalejší a složitější.

Druhý přístup k analýze OOPNs, kterým se v této práci zabýváme, je založen na generování a prohledávání stavových prostorů. Hlavním problémem těchto metod je problém stavové exploze - velikost stavového prostoru roste exponenciálně s velikostí modelu. Zkoumáme zde proto možnosti paralelního generování a procházení stavových prostorů na architekturách se sdílenou pamětí. Využití těchto architektur pro formální analýzu systémů je ojedinělé nejenom v kontextu
OOPNs, protože většina dosavadních prací se věnuje paralelizaci formální analýzy a verifikace systémů na architekturách s distribuovanou pamětí.

Pro usnadnění implementace obou výše uvedených metod byla navržena aplikace v jazyce Java, která integruje typový analyzátor s generátorem stavových prostorů OOPNs, čímž umožňuje znovupoužití částí společných oběma nástrojům. Typový analyzátor i generátor stavových prostorů OOPNs
byl implementován pouze prototypově pro ověření navržených principů. (Bohatost formalizmu OOPNs úplnou implementaci navržených metod v daném časovém horizontu ani neumožňuje.)

Hlavním přínosem této práce je návrh tří unikátních algoritmů pro formální analýzu OOPNs. Algoritmy pro statickou a dynamickou typovou analýzu, které využívají nové techniky pro práci s objekty a metodami pro vyřešení dosud otevřených problémů, jsou použitelné především v kontextu OOPNs. Naproti tomu algoritmus pro paralelní generování stavových prostorů na architekturách se sdílenou pamětí je principiálně použitelný pro širokou třídu modelovacích formalizmů. Hlavními přednostmi tohoto algoritmu je efektivní synchronizace přístupu ke sdílené vyhledávací tabulce a účinný způsob rozdělování práce mezi jednotlivé procesory, což jsou v kontextu paralelního zpracování stavových prostorů na architekturách se sdílenou pamětí unikátní mechanizmy.

Object-oriented Petri nets (OOPNs) have been developed (at our faculty) to support modelling, investigating, and prototyping concurrent object-oriented software systems. OOPNs join together Petri net concepts (causality, nondeterminism, and concurrency) with object orientation concepts (encapsulation, inheritance, and polymorphism). Objects and classes allow OOPNs to be used for creating large and well-arranged models which is a significant benefit for their practical usage. Formal analysis and verification of OOPN models is possible due their exact mathematical definition. It is, however, quite complex because OOPNs are a rich formalism. In this work, we concentrate on two analysis methods in the context of OOPNs.

Type Analysis

The first investigated method is type analysis. OOPNs - unlike many of the common dialects of high-level Petri nets - are not (syntactically) strongly typed which means that modellers do not have to explicitly declare the types of OOPN places, the types of the variables used in OOPN inscriptions, and so on. The goal of the type analysis is to automatically compute the types of tokens that can get to the particular places of an OOPN model. Weak typing of PNtalk is useful in the area of prototyping, however, as mentioned below, there are situations in which it may be useful to know at least something about the types associated with the particular OOPN places.

Type analysis can be understood as a special means of debugging OOPN models: modellers usually have some intuition about what types of tokens should get into particular OOPN places and if the results of a type analysis are different, there may be a fault in the model. The information derived from type analysis can also be used as a part of the documentation of a~model. Moreover, the results obtained from type analysis can further be useful when translating OOPNs into models described by some other - usually strongly typed - modelling
languages. Finally, the results which may be obtained from type analysis may be used to optimize the internal representation of OOPNs and thus to increase the efficiency of
running OOPN models and generating their state spaces.

In order to decrease time and space requirements of type analysis and to ensure its termination, we suitably approximate
the behaviour of OOPNs. The price which we pay for this is the fact that the sets of the types of tokens about which we are informed that they can get into the particular places can be bigger than in reality. However, it is a safe approximation and the obtained results can still be quite useful.

We have proposed two approaches to type analysis in OOPNs - the so-called static and dynamic type analysis. Both methods work with symbolically represented markings and events which do not contain concrete data values but the corresponding types only. Accordingly, we do not perform classical trivial computations in guards of transitions and ports or in actions of transitions. Instead, we only derive the types of the involved variables. Next, the multiplicities of elements in initial markings and arc expressions are ignored. Moreover, we do not remove types symbolically representing some tokens once they get into a place. The main difference between static and dynamic type analysis consist

objektově orientované Petriho sítě, PNtalk, formální metody, stavové prostory, problém stavové exploze, paralelizace, architektury se sdílenou pamětí, Java, JOMP

Object Oriented Petri Nets, PNtalk, Formal Methods, State Spaces, State Space Explosion Problem, Parallel Approach, Shared Memory Architecture, Java, JOMP

KŘENA, B.

20. 10. 2004

Brno

128

http://www.fit.vutbr.cz/~krena/prace/PhD.pdf, http://www.fit.vutbr.cz/~krena/prace/teze.pdf