Top

Published in:

2017 | OriginalPaper | Chapter

Model Checking in Parallel Logic Controllers Design and Verification

Authors : Michał Doligalski, Jacek Tkacz, Tomasz Gratkowski

Published in: Proceedings of the 2015 Federated Conference on Software Development and Object Technologies

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The parallel logic controllers (PLC) developing process can be both, simplified and improved by means of formal methods.

The paper presents approach based on Petri nets specification and model checking techniques used for formal verification, synthesis and implementation. Interpreted petri net (IPN) is selected as a formal behavioural model for parallel logic controllers. It is proposed to use graphical modelling tools for formal behavioural PLC modelling, authors ICPN is such example. The use of common standard, like Petri Net Markup Language (PNML) enables integration with formal analysis tools. The model is simplified (optimised) by means of formal reasoning system (Gentzen). The transformation of the simplified model is made automatically into VHDL description and NuSMV model. The resulting VHLD model can be used for simulation and next for synthesis and implementation. The reliability of the PLC is improved by formal verification. The paper presents the application of the additional specification described in the temporal logic. Model received from reasoning system can be verified by such specification. The formal verification enables to locate deviations from the specification. Proposed approach is useful especially in PLC rapid prototyping approach. The changes in the specification can be verified immediately, towards general specification requirements. Discrepancies between specification and the prototype are localised and can be removed before next iteration. Proposed approach improves visual analysis and fast modifications, ensuring high reliability of the constructed logic controller. The formal methods increases the reliability and quality of the parallel logic controller.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Memory Analysis and Performance Modeling for HPC Applications on Embedded Hardware via Instruction Accurate Simulation

next chapter Fuzzy Logic for Optimized Path Establishment in Optical Networks

Adamski, M., Tkacz, J.: Formal reasoning in logic design of reconfigurable controllers. In: Proceedings of 11th IFAC/IEEE International Conference on Programmable Devices and Embedded Systems PDeS 2012, Brno, Czech Republic, pp. 1–6 (2012)

Doligalski, M.: 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 2012, Brno, Czechy, pp. 80–83 (2012)

Doligalski, M., Adamski, M.: UML state machine implementation in FPGA devices by means of dual model and Verilog. In: 2013 11th IEEE International Conference on Industrial Informatics (INDIN), pp. 177–184 (2013)

Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers, New York (1985). http://www.cis.upenn.edu/∼jean/gbooks/logic.html

Girault, F., Pradin-Chezalviel, B., Kunzle, L., Valette, R.: Linear logic as a tool for reasoning on a Petri net model. In: INRIA/IEEE Symposium on Emerging Technologies and Factory Automation, ETFA 1995, vol. 1, pp. 49–57 (1995)

Grobelna, I.: Formal Verification of Logic Controller Specification by Means of Model Checking. Lecture Notes in Control and Computer Science. University of Zielona Góra Press, Zielona Góra (2013)

Grobelna, I., Grobelny, M., Adamski, M.: Model checking of UML activity diagrams in logic controllers design. In: Zamojski, W., Mazurkiewicz, J., Sugier, J., Walkowiak, T., Kacprzyk, J. (eds.) Proceedings of the Ninth International Conference on DepCoS-RELCOMEX. AISC, vol. 286, pp. 233–242. Springer, Heidelberg (2014)CrossRef

Karatkevich, A.: Dynamic Analysis of Petri Net-Based Discrete Systems. Lecture Notes in Control and Information Sciences, vol. 356. Springer-Verlag, Berlin (2007)MATH

Kozłowski, T., Dagless, E., Saul, J., Adamski, M., Szajna, J.: Parallel controller synthesis using Petri nets. In: IEEE Proceedings – Computers and Digital Techniques, vol. 142, no. 4, pp. 263–271 (1995)

10.

Leroux, H., Andreu, D., Godary-Dejean, K.: Handling exceptions in Petri net based digital architecture: from formalism to implementation on FPGAs. IEEE Trans. Ind. Inform. 99, 1 (2015)

11.

Lincoln, P., Shankar, N.: Proof search in first-order linear logic and other cut-free sequent calculi. In: Symposium on Logic in Computer Science, LICS 1994, pp. 282–291 (1994)

12.

Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRef

13.

Pereira, F., Gomes, L.: Automatic synthesis of VHDL hardware components from iopt Petri net models. In: Industrial Electronics Society, IECON 2013 - 39th Annual Conference of the IEEE, pp. 2214–2219, November 2013

14.

Rawski, M., Tomaszewicz, P., Borowik, G., Łuba, T.: 5 Logic synthesis method of digital circuits designed for implementation with embedded memory blocks of FPGAs. In: Adamski, M., Barkalov, A., Węgrzyn, M. (eds.) Design of Digital Systems and Devices. LNEE, vol. 79, pp. 121–144. Springer, Heidelberg (2011)CrossRef

15.

Tkacz, J., Adamski, M.: Logic design of structured configurable controllers. In: Proceedings of IEEE 3rd International Conference on Networked Embedded Systems for Every Application NESEA 2012, Liverpool, United Kingdom, p. 6 (2012)

16.

Wiśniewski, R., Stefanowicz, Ł., Bukowiec, A., Lipiński, J.: Theoretical aspects of Petri nets decomposition based on invariants and hypergraphs. In: Park, J.J.(.J.H.), Chen, S.-C., Gil, J.-M., Yen, N.Y. (eds.) Multimedia and Ubiquitous Engineering. LNEE, vol. 308, pp. 371–376. Springer, Heidelberg (2014)

Title: Model Checking in Parallel Logic Controllers Design and Verification
Authors: Michał Doligalski
Jacek Tkacz
Tomasz Gratkowski
Publisher: Springer International Publishing
Book: Proceedings of the 2015 Federated Conference on Software Development and Object Technologies
Print ISBN: 978-3-319-46534-0

Electronic ISBN: 978-3-319-46535-7

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-46535-7_3

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner