Structured Mapping of Petri Net States and Events for FPGA Implementations

• Autorzy: Tkacz J. , Adamski M.

Identyfikatory

DOI

10.2478/eletel-2013-0040

• Języki publikacji: EN

Abstrakty

EN

The paper presents a new method of structured encoding of global internal states and events in Reconfigurable Logic Controllers, which are directly mapped into Field Programmable Gate Arrays (FPGA). Modular, concurrently decomposed, colored state machine is chosen as a intermediate model, before the mapping of Petri net into an array structure of dedicated but very flexible and reliable digital system. The initial textual specification in formal Gentzen logic serves both as a design description for a rapid prototyping, as well as formal model, suitable for detailed computer-based reasoning about optimized and synthesized logic controller, implemented in configurable hardware. Only the selected linear subset from general, universal propositional Gentzen Logic is necessary to deduce several properties of the net, such as relations of nonconcurrency among structurally ordered macroplaces. The goal of this paper is to present the design methodology for modeling and synthesis of discrete controllers using related Petri net theory, rule-based theory (mathematical logic), and VHDL.

Słowa kluczowe

EN

configurable logic controllers; interpreted Petri net state space; local and global state encoding; hyperpgraph; logic design; Gentzen sequents; Petri net coloring; FPGA; VHDL

• Wydawca: Polish Academy of Sciences, Committee of Electronics and Telecommunication
• Czasopismo: International Journal of Electronics and Telecommunications
• Rocznik: 2013
• Tom: Vol. 59, No. 4
• Strony: 331--339
• Opis fizyczny: Bibliogr. 24 poz., il.

Twórcy

autor

Tkacz J.

• Institute of Computer Engineering and Electronics, University of Zielona Góra, Licealna 9, 65-417 Zielona Góra, Poland

autor

Adamski M.

• Institute of Computer Engineering and Electronics, University of Zielona Góra, Licealna 9, 65-417 Zielona Góra, Poland

Bibliografia

• [1] M. Adamski, A. Karatkevich, and M. Węgrzyn, Design of Embeded Control Systems. New York: Springer Science+Business Media, Inc., 2005.
• [2] J. Tkacz and M. Adamski, “Logic design of structured configurable controllers,” in Proceedings of IEEE 3rd International Conference on Networked Embedded Systems for Every Application NESEA’12, Liverpool, United Kingdom, 2012, p. 6.
• [3] M. Adamski and M. Węgrzyn, “Petri nets mapping into reconfigurable logic controllers,” Electronics and Telecommunications Quarterly, vol. 55, no. 2, pp. 157-182, 2009.
• [4] M. Adamski, “Specification and synthesis of Petri net based reprogrammable logic controller,” in Proceedings of 5th IFAC International Conference on Programmable Devices and Embedded Systems PDeS’01, Brno, Czech Republic, 2001, pp. 95-100.
• [5] K. Biliński, M. Adamski, J. Saul, and E. Dagless, “Petri-net-based algorithms for parallel-controller synthesis,” IEE Proceedings – Computers and Digital Techniques, vol. 141, no. 6, pp. 405-412, 1994.
• [6] M. Doligalski, “Behavioral specification of the logic controllers by means of the hierarchical configurable Petri nets,” in Proceedings of 11th IFAC/IEEE International Conference on Programmable Devices and Embedded Systems PDeS’12, Brno, Czech Republic, 2012, pp. 80-83.
• [7] Behavioral specification diversification for logic controllers implemented in FPGA devices, in Proceedings of the 9th Annual FPGA Conference – FPGAworld’12. Stockholm, Sweden: New York, ACM, 2012, p. 5.
• [8] C. Girault and R. Valk, Petri Nets for System Engineering: A Guide to Modeling, Verification, and Applications. Berlin/Heidelberg: Springer-Verlag, 2003.
• [9] A. Yakovlev, L. Gomes, and L. Lavagno, Hardware Design and Petri Nets. Boston: Kluwer, 2000.
• [10] K. Jensen, K. Kristensen, and L. Wells, “Coloured Petri nets and CPN tools for modelling and validation of concurrent systems,” International Journal on Software Tools for Technology Transfer (STTT), vol. 9, no. 3, pp. 213-254, 2007.
• [11] I. Grobelna, Formal Verifikation of Logic Controller Specification by Means of Model Checking, ser. Lecture Notes in Control and Computer Science. Zielona Góra: University of Zielona Góra Press, Poland, 2013.
• [12] M. Adamski and J. Tkacz, “Formal reasoning in logic design of reconfigurable controllers,” in Proceedings of 11th IFAC/IEEE International Conference on Programmable Devices and Embedded Systems PDeS’12, Brno, Czech Republic, 2012, pp. 1-6.
• [13] A. Bukowiec and M. Adamski, “Synthesis of Petri nets into FPGA with operation flexible memories,” in Proceedings of the IEEE 15th International Symposium on Design and Diagnostics of Electronic Circuits and Systems DDECS’12, Tallinn, Estonia, 2012, pp. 16-21.
• [14] J. H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving. New York: Harper & Row Publishers, 1985. [Online]. Available: http://www.cis.upenn.edu/jean/gbooks/logic.html.
• [15] T. Kozłowski, E. Dagless, J. Saul, M. Adamski, and J. Szajna, “Parallel controller synthesis using Petri nets,” IEE Proceedings – Computers and Digital Techniques, vol. 142, no. 4, pp. 263-271, 1995.
• [16] J. Tkacz and M. Adamski, “Calculation of state machine cover of safe Petri net by means of computer based reasoning,” Measurement Automation and Monitoring, vol. 57, no. 11, pp. 1397-1400, 2011.
• [17] J. Tkacz, “State machine type colouring of Petri net by means of using a symbolic deduction method,” Measurement Automation and Monitoring, vol. 53, no. 5, pp. 120-122, 2007.
• [18] T. Murata, “Petri nets: Properties, analysis and applications,” Proceedings of the IEEE, vol. 77, no. 4, pp. 541–580, 1989.
• [19] A. Karatkevich, Dynamic Analysis of Petri Net-Based Discrete Systems, ser. Lecture Notes in Control and Information Sciences. Berlin: Springer-Verlag, 2007, vol. 356.
• [20] M. Wiśniewska, R. Wiśniewski, and M. Adamski, “Usage of hypergraph theory in decomposition of concurrent automata,” Measurement Automation and Monitoring, vol. 53, no. 7, pp. 66-68, 2007.
• [21] H. Foster, A. Krolnik, and D. Lacey, Assertion-Based Design, 2nd ed. Norwell: Kluwer Academic Publishers, 2004.
• [22] G. Łabiak, M. Adamski, M. Doligalski, J. Tkacz, and A. Bukowiec, “UML modelling in rigorous design methodology for discrete controllers,” International Journal of Electronics and Telecommunications, vol. 58, no. 1, pp. 27-34, 2012.
• [23] A. Bukowiec, “Synthesis of FSMs based on architectural decomposition with joined multiple encoding,” International Journal of Electronics and Telecommunications, vol. 58, no. 1, pp. 35-41, 2012.
• [24] M. Doligalski, Behavioral Specification Diversification of Reconfigurable Logic Controllers, ser. Lecture Notes in Control and Computer Science. Zielona Góra: University of Zielona Góra Press, 2012, vol. 20.