Obiekt
Tytuł: Symboliczna analiza układów sterowania binarnego z wykorzystaniem wybranych metod analizy sieci Petriego
Streszczenie:
W pracy przedstawiono nową metodę analizy sterowników cyfrowych modelowanych z wykorzystaniem hierarchicznej sieci Petriego. Stosując proponowaną metodę, za pośrednictwem badania strukturalnych własności sieci odzwierciedlonych w postaci formuły Horna, uzyskuje się informacje o niezamierzonych defektach algorytmu sterowania procesem binarnym. Defekty przejawiające się w topologicznej strukturze sieci polegają na braku jej żywotności oraz wielokrotnym oznakowaniu tego samego miejsca (braku 1-ograniczoności, czyli bezpieczeństwa sieci). ; Komputerowa realizacja opracowanych metod stanowi ważną część rozwijanego w Instytucie Informatyki i Elektroniki Uniwersytetu Zielonogórskiego akademickiego systemu CAD wspomagającego projektowanie wspólbieżnych sterowników cyfrowych, implementowanych w programowalnych strukturach logicznych FPGA i CPLD. W pracy zamieszczono przyklad translacji sieci Petriego na równoważny model w języku opisu sprzętu Verilog-HDL. Wprowadzono nowy, użyteczny format PNSF3 regulowego opisu sterownika cyfrowego modelowanego hierarchiczną, interpretowaną, kolorowaną siecią Petriego. Obok szczegółowej weryfikacji modelu w dedykowanym środowisku wykorzystującym relacyjną bazę danych Oracle oraz technologie XML w połączeniu z grafiką SVG, proponuje się zastosowanie do tego celu również profesjonalnego pakietu Design/CPN. Końcowa symulacja sprawdzonego pod względem formalnym i poprawionego modelu może się również odbywać w nowoczesnym środowisku jezyków HDL, na przyklad Cadence Verilog-XL lub Aldec Active-HDL. ; Zasadnicza część metody analizy bazuje na algebrze Boole'a i symbolicznym przetwarzaniu danych. Ponieważ analizowana jest zredukowana sieć Petriego, abstrahowane zostają te podsieci, które nie mają wpływu na proces analizy lub nie są istotne na rozpatrywanym etapie projektu. Wartościowania spelniające zlożoną formułę klauzulową Horna określają pułapki i blokady wystepujące w badanej sieci. W przypadku badania żywotnosci bada się zależności pomiędzy blokadami i pułapkami, co zgodnie z dotychczasowym stanem wiedzy zawęża klasę analizowanych sieci, do AC i NSC. Dodatkowo wyznaczone P?niezmienniki wykorzystywane są między innymi do dekompozycji sieci na składowe automatowe i kodowania miejsc sieci. ; Proponowana metoda może również znaleźć zastosowanie w przemysłowych systemach bazujących na specyfikacji w języku graficznym SFC (Sequential Function Chart, norma IEC-1131-3).
Abstract:
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.
Wydawca:
Zielona Góra: Oficyna Uniwersytetu Zielonogórskiego
Format:
Identyfikator zasobu:
Jezyk:
Prawa do dysponowania publikacją:
Biblioteka Uniwersytetu Zielonogórskiego
Kolekcje, do których przypisany jest obiekt:
- Zielonogórska Biblioteka Cyfrowa > Repozytorium > Jednostki organizacyjne > Wydział Informatyki, Elektrotechniki i Automatyki
- Zielonogórska Biblioteka Cyfrowa > Repozytorium > Typy utworów > Rozprawy doktorskie
Data ostatniej modyfikacji:
2018-07-16
Data dodania obiektu:
2005-12-13
Liczba wyświetleń treści obiektu:
7 640
Liczba wyświetleń treści obiektu w formacie HTML
112
Wszystkie dostępne wersje tego obiektu:
https://zbc.uz.zgora.pl/publication/1915
