Detection of ladder program unstable states

• Autorzy: Grzybowski Michał , Młyńczak Jakub , Folęga Piotr , Sokołowska Lucyna , Pietruszczak Daniel

Identyfikatory

DOI

10.20858/tp.2023.19.3.09

• Języki publikacji: EN

Abstrakty

EN

This paper presents a modern method of detecting unstable states in ladder programs. Ladder programs are standard formalism used in a wide range of automation applications, especially in railway signaling systems. This formalism is characterized by a lack of explicit program control flow, which can result in the presence of unstable states. A state is unstable, if it leads to cyclic state transitions not anticipated by the designer (loop). The presence of unstable states is one of the possible program defects. This kind of defect is hard to detect and can harm program reliability. The presence of unstable states can be verified with formal methods by the construction of a ladder program model and analysis of its properties. The authors propose a method of static analysis of ladder programs by translating them into predicate logic formulas and construction of formulas expression stability of the program, which can be analyzed with SAT solvers. The presented method allows for automatic verification of the presence of unstable states in the program. The method is conservative (i.e., it concludes that the program has no unstable states only if it is the case). Preliminary experiments performed by authors with a Z3 solver indicate that the method is suitable for use for verification of interlocking programs of computer-based railway signaling systems.

Słowa kluczowe

EN

ladder programs; formal methods; static analysis

PL

programy drabinkowe; metody formalne; analiza statyczna

• Wydawca: Wydawnictwo Politechniki Śląskiej
• Czasopismo: Transport Problems
• Rocznik: 2024
• Tom: T. 19, z. 3
• Strony: 107--119
• Opis fizyczny: Bibliogr. 20 poz.

Twórcy

autor

Grzybowski Michał

• Silesian University of Technology, Faculty of Transport and Aviation Engineering; Krasińskiego 8, 40-019 Katowice, Poland

• https://orcid.org/0000-0002-4841-147X

autor

Młyńczak Jakub

• Silesian University of Technology, Faculty of Transport and Aviation Engineering; Krasińskiego 8, 40-019 Katowice, Poland

• https://orcid.org/0000-0003-2947-7980

autor

Folęga Piotr

• Silesian University of Technology, Faculty of Transport and Aviation Engineering; Krasińskiego 8, 40-019 Katowice, Poland

• https://orcid.org/0000-0001-6775-7559

autor

Sokołowska Lucyna

• Railway Research Institute IK; Józefa Chłopickiego 50, 04-275 Warsaw, Poland

• https://orcid.org/0000-0002-0699-4312

autor

Pietruszczak Daniel

• Casimir Pulaski Radom University, Faculty of Transport, Electrical Engineering and Computer Science Malczewskiego 29, 26-600 Radom, Poland

• https://orcid.org/0000-0001-8943-0805

Bibliografia

• 1. Huang, L. The Past, Present and Future of Railway Interlocking System. In: 2020 IEEE 5th International Conference on Intelligent Transportation Engineering. Beijing: Curran Associates. Inc. 2020. P. 170-174.
• 2. Hagelin, G. ERICSSON Safety System for Railway Control. In: Software Diversity in Computerized Control Systems. Springer. 1998. P. 11-21.
• 3. Lindqvist, L. & Jadhav, R. Application of communication based Moving Block system on existing metro lines. WIT Transactions on State of the Art in Science and Engineering. 2010. Vol. 46. P. 55-64.
• 4. Roussel, J.M. & Denis, B. Safety properties verification of ladder diagram programs. Journal Européen des Systèmes Automatisés (JESA). 2002. Vol. 36. No. 7. P. 905-917.
• 5. Belo Lourenço, C. & Cousineau, D. & Faissole, F. & Marché, C. & Mentré D. & Inoue, H. Automated formal analysis of temporal properties of Ladder programs. International Journal on Software Tools for Technology Transfer. 2022. Vol. 24. No. 6. P. 977-997.
• 6. Su, Z. Automatic Analysis of Relay Ladder Logic Programs. Report No. UCB/CSD-97-969. Berkeley: University of California. 1997. P. 1-26.
• 7. Aiken, A. & Manuel, F. & Su, Z. Detecting races in Relay Ladder Logic programs. International Journal on Software Tools for Technology Transfer. 2000. Vol. 3. No. 1. P. 93-105.
• 8. da Silva Oliveira, E.A. & da Silva, L.D. & Gorgônio, K. & Perkusich, A. & Martins, A.F. Obtaining formal models from Ladder diagrams. In: 2011 9th IEEE International Conference on Industrial Informatics. Lisbon: IEEE. 2011. P. 796-801.
• 9. Chen, X. & Luo, J. & Qi, P. Method for translating ladder diagrams to ordinary 0 nets. In: 2012 IEEE 51st IEEE Conference on Decision and Control (CDC). Maui: IEEE. 2012. P. 6716-6721.
• 10. Luo, J. & Zhang, Q. & Chen, X. & Zhou, M. Modeling and Race Detection of Ladder Diagrams via Ordinary Petri Nets. IEEE Transactions on Systems, Man, and Cybernetics: Systems. 2018. Vol. 48. No. 7. P. 1166-1176.
• 11. Kanso, K. & Moller, F. & Setzer, A. Automated Verification of Signalling Principles in Railway Interlocking Systems. Electronic Notes in Theoretical Computer Science. 2009. Vol. 250 No. 2. P. 19-31.
• 12. Petersen, J.L. Methods for Validating Railway Interlocking Systems. PhD thesis. Kongens Lyngby: Technical University of Denmark. 1998.
• 13. Borälv, A. Case Study: Formal Verification of a Computerized Railway Interlocking. Formal Aspects of Computing. 1998. Vol. 10. No. 4. P. 338-360.
• 14. Claessen, K. & Een, N. & Sheeran, M. & Sörensson, N. & Voronov, A. & Åkesson, K. SAT-Solving in Practice, with a Tutorial Example from Supervisory Control. Discrete Event Dynamic Systems. 2009. Vol. 19. No. 4. P. 495-524.
• 15. Alouneh, S. & Abed, S. & Al Shayeji, M.H. & Mesleh, R. A comprehensive study and analysis on SAT-solvers: advances, usages and achievements. Artificial Intelligence Review. 2019. Vol. 52. No. 4. P. 2575-2601.
• 16. de Moura, L. & Bjørner, N. Z3: An Efficient SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems. Budapest: Springer. 2008. P. 337-340.
• 17. Walker, M. & Bissell, C. & Monk, J. The PLC: A Logical Development. Measurement and Control. 2010. Vol. 43. No. 9. P. 280-284.
• 18. Mesli-Kesraoui, S. & Goubali, O. & Kesraoui, D. & Eloumami, I. & Oquendo, F. Formal Verification of the Race Condition Vulnerability in Ladder Programs. In: 2020 IEEE Conference on Control Technology and Applications (CCTA). Montreal. 2020. P. 892-897.
• 19. Boukala, M.C. & Petrucci, L. Distributed model-checking and counterexample search for CTL logic. International Journal of Critical Computer-Based Systems 3. 2012. Vol. 3. No. 1-2. P. 44-59.
• 20. Dąbrowa-Bajon, M. Podstawy sterowania ruchem kolejowym. [In Polish: Basics of rail traffic control]. Third Edition. Warsaw: Publishing House of the Warsaw University of Technology. 2014. 391 p.