Namn:
Henrik Friman

Titel:
Petri Net Class Library and Translation from PRES+ to Timed Automata

Abstract:

Many systems are nowadays very complex and every component is itself
equally complex and so is its communication with other
components. Regardless of what system to be modelled, there are
several properties, common for all models, that a usable modelling
language should have. Such systems typically consist of synchronised
interacting components, with their own states. Petri nets are designed
specifically to model this kind of systems. In this thesis a library,
which can easily be extended to be able to cope with many different
types of Petri nets, has been developed and implemented.

Petri nets are today a fairly well studied model and several
properties of Petri nets are well known. The thesis covers modules,
able to check various Petri net properties, that have been
implemented.

There exist several specialisations of Petri nets. One such Petri net
formalism, called PRES+, has especially been developed for modelling
embedded systems. There is a model checking tool available for
validation and verification of real-time systems modelled as networks
of timed automata. For the purpose of being able to check properties
of PRES+ models, a translation procedure from PRES+ to timed automata
has previously been developed. As part of this thesis this translation
procedure has also been implemented.

Tid:
torsdagen den 27/2 kl.17

Plats:
John von Neumann

Antal poäng:
20 p




Juha Takkinen, <juhta@ida.liu.se>