A1 - Węgrzyn, Agnieszka
PB - Zielona Góra: Oficyna Uniwersytetu Zielonogórskiego
N2 - Determining whether the Petri net is live is very important, because a good system should not contain events, which can never occur. Testing the liveness (boundedness) of Petri net depend on finding deadlock and traps and researching dependence between theirs. Within of a framework of project prepared a new method analysis of digital controllers modeled using hierarchical Petri nets. A Petri nets is a mathematical object that exists independently of any physical representation. The nets can effectively describe parallelism. Their graphical form is used as a tool for the modeling and analysis of digital circuits, especially concurrent controllers.
N2 - During reduction of Petri net are removed such parts of Petri net that does not influenced analysis process. Such Petri net is presented as Horn formula. A Horn formula is a conjunction of basic Horn formulae. The basic Horn formula (Horn clause) is a disjunction of literals, with at most one positive literal. The obtained Horn formula is solved using Thelen's algorithm that is based on prime implicants. A prime implicant algorithm is used the method of Nelson, who has shown that all prime implicants of a function f are obtained when arbitrary conjunctive form F of f is expanded into a disjunctive form by multiplying out the disjunctions of F and deleting products that subsume others. Results of Horn formulae determine traps and deadlocks. In case of testing liveness are checked dependences between traps and deadlocks. In case of testing boudedness is checked if deadlock is a trap (P?invariants). P?invariants are used for decompositions and colorings Petri nets. On the other hand, to do such verification algorithm is implemented in PeNCAD system developed at University of Zielona Góra.
N2 - In the project, a new way of modeling and simulation of Petri nets is prepared too. The new language XML, for modeling Petri nets gives a new possibility. The advantage of XML-based format is a possibility of data exchange between various tools and various representations of concurrent controllers. Using such an approach, direct transformation from SFC model into Petri net model and simulation of Petri nets and SFC is possible. There are different methods of verification modeled systems. One of the simplest methods is simulation. It is similar to the debugging of program execution. During the simulation it is possible to check whether a circuit modeled by a Petri net and SFC behaves correctly. Therefore, it is possible to recognize and remove errors in the controllers, even at an early stage of the design.
KW - sieci Petriego
KW - modelowanie
KW - rozprawa doktorska
KW - nauki techniczne
KW - formuły Horna
KW - sieci SFC
KW - algorytm SLT
KW - język XML
KW - język PNSF3
KW - symulacja
KW - system PeNCAD
T1 - Symboliczna analiza układów sterowania binarnego z wykorzystaniem wybranych metod analizy sieci Petriego