Dane o rozprawie doktorskiej

Rodzaj pracy	Rozprawa doktorska
Data uzyskania stopnia	27 stycznia 2004
Uzyskany stopien naukowy	doktor nauk technicznych
Promotor	prof. zw. dr hab. inz. Marian Adamski, Uniwersytet Zielonogórski, Instytut Informatyki i Elektroniki
Recenzenci	Prof. Tadeusz Luba, Politechnika Warszawska, Instytut Telekomunikacji Prof. Edward Hrynkiewicz, Poltechnika Slaska, Instytut Elektroniki
Jednostka prowadzaca przewód	Politechnika Warszawska, Wydzial Elektroniki i Technik Informacyjnych
Miejsce pracy autora rozprawy	Uniwersytet Zielonogórski, Wydzial Elektrotechniki, Informatyki i Telekomunikacji
Dziedzina naukowa	Nauki techniczne
Dyscyplina naukowa	Informatyka
Specjalnosc naukowa	Informatyka
Sposób zgloszenia rozprawy, dostepnosc, liczba stron	Nie ogloszono, Biblioteka Glówna Politechniki Warszawskiej, s.148; zbc.uz.zgora.pl
Wydawca	Oficyna Wydawnicza Uniwersytetu Zielonogórskiego
Slowa kluczowe	sterowniki binarne, sieci Petriego, analiza, modelowanie, FPGA

Streszczenie

W pracy przedstawiono nowa metode analizy sterowników cyfrowych modelowanych z wykorzystaniem hierarchicznej sieci Petriego. Stosujac proponowana metode, za posrednictwem badania strukturalnych wlasnosci sieci odzwierciedlonych w postaci formuly Horna, uzyskuje sie informacje o niezamierzonych defektach algorytmu sterowania procesem binarnym. Defekty przejawiajace sie w topologicznej strukturze sieci polegaja na braku jej zywotnosci oraz wielokrotnym oznakowaniu tego samego miejsca (braku 1-ograniczonosci, czyli bezpieczenstwa sieci).

Komputerowa realizacja opracowanych metod stanowi wazna czesc rozwijanego w Instytucie Informatyki i Elektroniki Uniwersytetu Zielonogórskiego akademickiego systemu CAD wspomagajacego projektowanie wspólbieznych sterowników cyfrowych, implementowanych w programowalnych strukturach logicznych FPGA i CPLD. W pracy zamieszczono przyklad translacji sieci Petriego na równowazny model w jezyku opisu sprzetu Verilog-HDL. Wprowadzono nowy, uzyteczny format PNSF3 regulowego opisu sterownika cyfrowego modelowanego hierarchiczna, interpretowana, kolorowana siecia Petriego. Obok szczególowej weryfikacji modelu w dedykowanym srodowisku wykorzystujacym relacyjna baze danych Oracle oraz technologie XML w polaczeniu z grafika SVG, proponuje sie zastosowanie do tego celu równiez profesjonalnego pakietu Design/CPN. Koncowa symulacja sprawdzonego pod wzgledem formalnym i poprawionego modelu moze sie równiez odbywac w nowoczesnym srodowisku jezyków HDL, na przyklad Cadence Verilog-XL lub Aldec Active-HDL.
           Zasadnicza czesc metody analizy bazuje na algebrze Boole'a i symbolicznym przetwarzaniu danych. Poniewaz analizowana jest zredukowana siec Petriego, abstrahowane zostaja te podsieci, które nie maja wplywu na proces analizy lub nie sa istotne na rozpatrywanym etapie projektu. Wartosciowania spelniajace zlozona formule klauzulowa Horna okreslaja pulapki i blokady wystepujace w badanej sieci. W przypadku badania zywotnosci bada sie zaleznosci pomiedzy blokadami i pulapkami, co zgodnie z dotychczasowym stanem wiedzy zaweza klase analizowanych sieci, do AC i NSC. Dodatkowo wyznaczone P‑niezmienniki wykorzystywane sa miedzy innymi do dekompozycji sieci na skladowe automatowe i kodowania miejsc sieci.
           Proponowana metoda moze równiez znalezc zastosowanie w przemyslowych systemach bazujacych na specyfikacji w jezyku graficznym SFC (Sequential Function Chart, norma IEC-1131-3).

Abstact

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.

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.

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.