Wykrywanie zastojów w sterownikach logicznych metodą symbolicznego wnioskowania Gentzena

• Autorzy: Tkacz J.

Warianty tytułu

EN

Deadlocks detection in logic controllers by means of using Gentzen symbolic deduction

• Konferencja: Konferencja Informatyka - Sztuka czy Rzemiosło (19-22 czerwca 2006; Złotniki Lubańskie; Polska)
• Języki publikacji: PL

Abstrakty

PL

W referacie przedstawiono koncepcję i sposób weryfikacji specyfikacji sterowników logicznych z wykorzystaniem wnioskowania Gentzena. Zastosowanie symbolicznej metody Gentzena w odróżnieniu od opisywanych w literaturze rozwiązań, pozwala na pominięcie szeregu kroków w procesie analizy symbolicznej sieci Petriego, opisującej funkcjonowanie sterownika, co prowadzi do pełnej automatyzacji procesu weryfikacji. Metoda dokładnie określa fragmenty specyfikacji, w których występują defekty (np. zastoje).

EN

The paper presents a concept and methodology for verification of logic control-lers specification by means of using Gentzen symbolic deduction. This method omits some steps of algorithm of Petri net symbolic analysis, where Petri net specifies behavior of logic controller. This concept makes possible to automate full process of verification and determines places, for which specification has errors (deadlocks).

Słowa kluczowe

PL

Gentzen; sekwent; wnioskowanie symboliczne; sterowniki logiczne; sieci Petriego

EN

Gentzen; sequent; symbolic deduction; logic controllers; Petri nets

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2006
• Tom: R. 52, nr 6 bis
• Strony: 11--13
• Opis fizyczny: Bibliogr. 10 poz.

Twórcy

autor

Tkacz J.

• Instytut Informatyki i Elektroniki, Uniwersytet Zielonogórski,

Bibliografia

• [1] Adamski M.: Projektowanie układów cyfrowych systematyczną metodą strukturalną, Wydawnictwo Wyższej Szkoły Inżynierskiej w Zielonej Górze, Zielona Góra 1990.
• [2] Adamski M.: Parallel Controller Implementation using Standard PLD Software. FPGAs. Abingdon, England 1991, pp. 296-304.
• [3] Barkaoui K., Minoux M.: A polynomial-time graph algorithm to decide liveness of some basic classes of bounded Petri nets. Lecture Notes in Com-puter Science, Berlin 1992:Springer Verlag, Vol. 616, ss. 62-75.
• [4] Commoner F.: Deadlocks in Petri Nets. - Wakefield 1972: Applied Data Res. Inc.
• [5] Mathony H. J.: Uniwersal logic design algorithm and its application the synthesisof two-lewel switching circuits. IEE Proceedings Letters, Elsevier Science Publishers (North Holland),Vol. 29,1990, pp. 195-210.
• [6] Murata T.: Petri nets: properties, analysis and applications. Proceedings of the IEEE 1989, Vol.77, No. 4, ss. 541-580.
• [7] Suraj Z., Szpyrka M.: Sieci Petriego I PN-Tools. Wydawnictwo Wyższej Szkoły Pedagogicznej, Rzeszów 1999.
• [8] Pawlak Z.: Automatyczne dowodzenie twierdzeń. Państwowe Zakłady Wydawnictw Szkolnych, Warszawa 1965.
• [9] Tkacz J.: Komputerowe wspomaganie przekształceń symbolicznych Gentzena. Metody i systemy komputerowe w badaniach naukowych i projektowaniu inżynierskim : IV Krajowa konferencja. Kraków, Polska, 2003, ss. 113-116.
• [10] Węgrzyn A.: Symboliczna analiza układów sterowania binarnego z wykorzystaniem wybranych metod analizy sieci Petriego. Wydawnictwo Politechniki Zielonogórskiej, Zielona Góra 1996.