Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Software and Systems Modeling
Erschienen in: Software and Systems Modeling 4/2016

25.12.2014 | Theme Section Paper

An overview of model checking practices on verification of PLC software

verfasst von: Tolga Ovatman, Atakan Aral, Davut Polat, Ali Osman Ünver

Erschienen in: Software and Systems Modeling | Ausgabe 4/2016

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Programmable logic controllers (PLCs) are heavily used in industrial control systems, because of their high capacity of simultaneous input/output processing capabilities. Characteristically, PLC systems are used in mission critical systems, and PLC software needs to conform real-time constraints in order to work properly. Since PLC programming requires mastering low-level instructions or assembly like languages, an important step in PLC software production is modelling using a formal approach like Petri nets or automata. Afterward, PLC software is produced semiautomatically from the model and refined iteratively. Model checking, on the other hand, is a well-known software verification approach, where typically a set of timed properties are verified by exploring the transition system produced from the software model at hand. Naturally, model checking is applied in a variety of ways to verify the correctness of PLC-based software. In this paper, we provide a broad view about the difficulties that are encountered during the model checking process applied at the verification phase of PLC software production. We classify the approaches from two different perspectives: first, the model checking approach/tool used in the verification process, and second, the software model/source code and its transformation to model checker’s specification language. In a nutshell, we have mainly examined SPIN, SMV, and UPPAAL-based model checking activities and model construction using Instruction Lists (and alike), Function Block Diagrams, and Petri nets/automata-based model construction activities. As a result of our studies, we provide a comparison among the studies in the literature regarding various aspects like their application areas, performance considerations, and model checking processes. Our survey can be used to provide guidance for the scholars and practitioners planning to integrate model checking to PLC-based software verification activities.
Vorheriger Artikel Theme issue on Integrated Formal Methods
Nächster Artikel Model-checking software library API usage rules

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Fußnoten
1
Papers that do not include explicit information were omitted.
Table 3
A classification of studies performed with textual PLC programs
 
App. area
Syst. size
Performance
Auto. level
Formal spec.
[113]
N/A
18 lines
N/A
Automatic
N/A
[16]
Tool changing
89 lines
N/A
Automatic
Manual
[77]
Batch plant
N/A
Minutes
Manual
Manual
[41]
N/A
4000 vars
Seconds
Automatic
N/A
[90]
Counter
N/A
Minutes–hours
Semiauto.
Manual
[100]
Counter
N/A
Seconds
Automatic
Manual
[118]
N/A
N/A
N/A
Automatic
Manual
Table 4
Properties checked when model checking textual PLC programs
 
Real time
Correctness
Spec. logic
 
Invariance
Safety
Liveness
[16]
No
Yes
Yes
Yes
LTL
[77]
No
Yes
No
No
LTL
[100]
No
Yes
No
No
CTL
[118]
Yes
Yes
No
No
CTL
 
2
Papers that do not include explicit information were omitted.
Table 5
A classification of studies performed with FBDs
 
App. area
Syst. size
Performance
Auto. level
Formal spec.
[59]
Nuclear plant
16 blocks 7 vars
N/A
Semiauto.
N/A
[20]
Hydrogen gen. Unit
19 blocks 12 vars
N/A
Automatic
N/A
[115]
Nuclear plant
1,500 blocks 1,000 vars
N/A
Automatic
Manual
[89]
Railway interlock
100 vars
Minutes
Automatic
Manual
[103]
Safety app.
6 blocks
N/A
Automatic
N/A
[29, 30]
Train control
30 blocks
\(<\)1 s
Automatic
Automatic
[57]
Nuclear plant
20,000 blocks 9,000 vars
N/A
Automatic
N/A
[87]
N/A
N/A
N/A
Manual
Manual
Table 6
Properties checked when model checking FBD-based PLC programs
 
Real time
Correctness
Spec. logic
 
Invariance
Safety
Liveness
[89]
No
No
Yes
No
CTL
[29, 30]
No
Yes
Yes
No
CTL
[57]
No
Yes
Yes
No
N/A
 
3
Papers that do not include explicit information were omitted.
 
4
Timed Net C/E’s actually use Petri nets in representation of internal dynamics. Nevertheless, we will be discussing them together with other condition/event system-based approaches.
 
7
Esterel Technologies, SCADE Suite Product Description: http://​www.​esterel-technologies.​com/​products/​scade-suite/​.
 
Literatur
1.
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)MATH
2.
3.
4.
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuéllar, J., Drielsma, P.H., Héam, P.C., Kouchnarenko, O., Mantovani, J., et al.: The avispa tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification, pp. 281–285. Springer, Berlin (2005)
5.
Barbosa, H., Déharbe, D.: Formal verification of plc programs using the b method. In: Abstract State Machines, Alloy, B, VDM, and Z, pp. 353–356. Springer, Berlin (2012)
6.
Bauer, N., Huuck, R.: Towards automatic verification of embedded control software. In: Proceedings of Second Asia-Pacific Conference on Quality Software, pp. 375–383 (2001). doi:10.​1109/​APAQS.​2001.​990043
7.
Bauer, N., Engell, S., Huuck, R., Lohmann, S., Lukoschus, B., Remelhe, M., Stursberg, O.: Verification of plc programs given as sequential function charts. In: Integration of Software Specification Techniques for Applications in Engineering, Lecture Notes in Computer Science, vol. 3147, chap. 28, pp. 517–540. Springer, Berlin (2004) DOI:10.​1007/​978-3-540-27863-4_​28
8.
Bender, D.F., Combemale, B., Crgut, X., Farines, J.M., Berthomieu, B., Vernadat, F.: Ladder metamodeling and plc program validation through time petri nets. In: Schieferdecker, I., Hartman, A. (eds.) Model Driven Architecture Foundations and Applications, Lecture Notes in Computer Science, vol. 5095, pp. 121–136. Springer, Berlin (2008)CrossRef
9.
Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool tina-construction of abstract state spaces for petri nets and time petri nets. Int. J. Prod. Res. 42(14), 2741–2756 (2004)CrossRefMATH
10.
Biallas, S., Brauer, J., Kowalewski, S.: Arcade.plc: a verification platform for programmable logic controllers. In: 2012 Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 338–341 (2012). doi:10.​1145/​2351676.​2351741
11.
Bochot, T., Virelizier, P., Waeselynck, H., Wiels, V.: Model checking flight control systems: the airbus experience. ICSE Companion, pp. 18–27 (2009)
12.
Bornot, S., Huuck, R., Lukoschus, B., Lakhnech, Y.: Verification of sequential function charts using smv. In: In PDPTA 2000: International Conference on Parallel and Distributed Processing Techniques and Applications, Las Vegas, pp. 2987–2993 (2000)
13.
Brayton, R.K., Hachtel, G.D., Sangiovanni-Vincentelli, A., Somenzi, F., Aziz, A., Cheng, S.T., Edwards, S., Khatri, S., Kukimoto, Y., Pardo, A.: Vis: a system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification, pp. 428–432. Springer, Berlin (1996)
14.
Brinksma, E., Mader, A.: Verification and optimization of a plc control schedule. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN Model Checking and Software Verification, pp. 73–92. Springer, Berlin (2000)
15.
Budha, M., Thapa, D., Park, S., Wang, G.N.: Generation of plc ladder diagram using modular structure. In: 2008 International Conference on Computational Intelligence for Modelling Control Automation, pp. 1194–1198 (2008). doi:10.​1109/​CIMCA.​2008.​125
16.
Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of plc programs written in instruction list. In: IEEE International Conference on Systems, Man, and Cybernetics, vol. 4, pp. 2449–2454. IEEE (2000)
17.
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: Nusmv: a new symbolic model verifier. In: Computer Aided Verification. Springer, Berlin, pp 495–499 (1999)
18.
Cofer, D.D., Whalen, M.W., Miller, S.P.: Model-checking of safety-critical software for avionics. ERCIM News 75 (2008)
19.
Couffin, S.L., Lesage, J.J.: Formal verification of the sequential part of plc programs. In: Boel, R., Stremersch, G. (eds) Discrete Event Systems. Springer, Berlin, pp. 247–254 (2000)
20.
da Silva, L.D., de Assis Barbosa, L.P., Gorgonio, K., Perkusich, A., Lima, A.M.N.: On the automatic generation of timed automata models from function block diagrams for safety instrumented systems. In: 34th Annual Conference of IEEE Industrial Electronics, IECON 2008, pp. 291–296 (2008). doi:10.​1109/​IECON.​2008.​4757968
21.
Dacharry, H.P., Giambiasi, N.: A formal verification approach for devs. In: Proceedings of the 2007 Summer Computer Simulation Conference, Society for Computer Simulation International, SCSC ’07, San Diego, CA, USA, pp. 312–319 (2007)
22.
de Assis Barbosa, L.P., Gorgonio, K., da Silva, L.D., Lima, A.M.N., Perkusich, A.: On the automatic generation of timed automata models from isa 5.2 diagrams. In: IEEE Conference on Emerging Technologies and Factory Automation, 2007. ETFA, IEEE, pp. 406–412 (2007)
23.
de Vasconcelos Oliveira, K., da Silva, L.D., Perkusich, A., Lima, A.M.N., Gorgônio, K.: Automatic timed automata extraction from ladder programs for model-based analysis of control systems. In: IEEE International Symposium on Industrial Electronics (ISIE), pp. 90–95. IEEE (2010)
24.
Dierks, H.: Plc-automata: a new class of implementable real-time automata. In: Bertran, M., Rus, T. (eds.) Transformation-Based Reactive Systems Development, pp. 111–125. Springer, Berlin (1997)
25.
26.
Dierks, H.: Comparing model checking and logical reasoning for real-time systems. Form. Asp. Comput. 16(2), 104–120 (2004)CrossRefMATH
27.
Dierks, H., Tapken, J.: Tool-supported hierarchical design of distributed real-time systems. In: Proceedings of 10th Euromicro Workshop on Real-Time Systems, pp. 222–229. IEEE (1998)
28.
Dill, D.L.: The murphi verification system. In: Proceedings of the 8th International Conference on Computer Aided Verification, CAV ’96, pp. 390–393. Springer, London (1996)
29.
Enoiu, E.P., Doganay, K., Bohlin, M., Sundmark, D., Pettersson, P.: Mos: an integrated model-based and search-based testing tool for function block diagrams. In: 1st International Workshop on Combining Modelling and Search-Based Software Engineering (CMSBSE), pp. 55–60 (2013a). doi:10.​1109/​CMSBSE.​2013.​6605711
30.
Enoiu, E.P., Sundmark, D., Pettersson, P.: Model-based test suite generation for function block diagrams using the uppaal model checker. In: Proceedings of Sixth IEEE International Conference on Software Testing, Verification and Validation. IEEE (2013b)
31.
Faivre, A., Benoit, P.: Safety critical software of meteor developed with the B formal method and the vital coded processor. In: WCRR’99, World Congress on Railway Research, Tokyo, Japan (1999)
32.
Fantechi, A., Gnesi, S.: On the adoption of model checking in safety-related software industry. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) Computer Safety, Reliability, and Security, pp. 383–396. Springer, Berlin (2011)
33.
Farines, J.M., de Queiroz, M.H., da Rocha, V.G., Carpes, A.M.M.: A model-driven engineering approach to formal verification of plc programs. In: IEEE 16th Conference on Emerging Technologies Factory Automation (ETFA), pp. 1–8 (2011). doi:10.​1109/​ETFA.​2011.​6058983
34.
35.
Frey, G.: Hierarchical design of logic controllers using signal interpreted petri nets. In: Proceedings of the IFAC Conference on Analysis and Design of Hybrid Systems, p. 12 (2003)
36.
Frey, G., Litz, L.: Verification and validation of control algorithms by coupling of interpreted petri nets. In: 1998 IEEE International Conference on Systems, Man, and Cybernetics. vol 1, pp. 7–12. IEEE (1998)
37.
Frey, G., Litz, L.: Formal methods in plc programming. In: IEEE International Conference on Systems, Man, and Cybernetics, vol. 4, pp. 2431–2436. IEEE (2000)
38.
Frey, G., Wagner, F.: A toolbox for the development of logic controllers using petri nets. In: 8th International Workshop on Discrete Event Systems, pp. 473–474. IEEE (2006)
39.
Fujino, K., Imafuku, K., Yuh, Y., Hirokazu, N.: Design and verification of the sfc program for sequential control. Comput. Chem. Eng. 24(2), 303–308 (2000)CrossRef
40.
Gergely, E.I., Coroiu, L., Gacsadi, A.: Design of safe plc programs by using petri nets and formal methods. In: 11th WSEAS International Conference on Automation and Information, Romania, pp. 86–91 (2010)
41.
Gourcuff, V., Smet, O.D., Faure, J.M.: Efficient representation for formal verification of plc programs. In: 8th International Workshop on Discrete Event Systems, pp. 182–187. IEEE (2006)
42.
Grobelna, I.: Formal verification of embedded logic controller specification with computer deduction in temporal logic. Electr. Rev. 12a, 47–50 (2011)
43.
Grobelna, I.: Control interpreted petri nets-model checking and synthesis. In: Pawlewski, P. (ed.) Petri Nets—Manufacturing and Computer Science. InTech, Rijeka (2012). doi:10.​5772/​47797
44.
Grobelna, I., Adamski, M.: Model checking of control interpreted petri nets. In: Proceedings of the 18th International Conference Mixed Design of Integrated Circuits and Systems (MIXDES), pp. 621–626. IEEE (2011)
45.
Halbwachs, N., Lagnier, F., Ratel, C.: Programming and verifying real-time systems by means of the synchronous data-flow language lustre. IEEE Trans. Softw. Eng. 18(9), 785–793 (1992)CrossRefMATH
46.
Hall, A.: Seven myths of formal methods. Softw. IEEE 7(5), 11–19 (1990)CrossRef
47.
Hanisch, H.M., Thieme, J., Luder, A., Wienhold, O.: Modeling of plc behavior by means of timed net condition/event systems. In: 1997 6th International Conference on Emerging Technologies and Factory Automation Proceedings, ETFA’97, pp. 391–396. IEEE (1997)
48.
49.
Havelund, K., Lowry, M., Park, S., Pecheur, C., Penix, J., Visser, W., White, J., et al.: Formal analysis of the remote agent before and after flight. In: Proceedings of the 5th NASA Langley Formal Methods Workshop, vol. 134 (2000)
50.
Heimdahl, M.P., Rayadurgam, S., Visser, W., Devaraj, G., Gao, J.: Auto-generating test sequences using model checkers: a case study. In: Formal Approaches to Software Testing, pp. 42–59. Springer, Berlin (2004)
51.
Heiner, M., Menzel, T.: A petri net semantics for the plc language instruction list. In: Workshop on Discrete Event Systems (WODES 98), pp. 161–166 (1998)
52.
Henzinger, T.A., Ho, P.H., Wong-Toi, H.: A user guide to hytech. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 41–71. Springer, Berlin (1995)
53.
54.
Huuck, R.: Software verification for programmable logic controllers. Ph.D. thesis, University of Kiel (2003)
55.
Huuck, R., Lukoschus, B., Bauer, N.: A model-checking approach to safe sfcs. In: IMACS Multiconference on Computational Engineering in Systems Applications (2003)
56.
James, P., Lawrence, A., Moller, F., Roggenbach, M., Seisenberger, M., Setzer, A., Kanso, K., Chadwick, S.: Verification of solid state interlocking programs. In: Counsell, S., Nez, M. (eds.) Software Engineering and Formal Methods, Lecture Notes in Computer Science, pp. 253–268. Springer, Berlin (2014). doi:10.​1007/​978-3-319-05032-4-19
57.
Jee, E., Jeon, S., Cha, S.D., Koh, K.Y., Yoo, J., Park, G.Y., Seong, P.H.: Fbdverifier: interactive and visual analysis of counterexample in formal verification of function block diagram. J. Res. Pract. Inf. Technol. 42(3), 171–188 (2010)
58.
59.
Jeon, S.: Verification of function block diagram through Verilog translation. Master’s thesis, KAIST, Republic of Korea (2007)
60.
Jiménez-Fraustro, F., Rutten, É.: A synchronous model of iec 61131 plc languages in signal. In: 13th Euromicro Conference on Real-Time Systems, pp. 135–142. IEEE (2001)
61.
John, K.H., Tiegelkamp, M.: IEC 61131–3: Programming Industrial Automation Systems: Concepts and Programming Languages, Requirements for Programming Systems, Decision-Making Aids. Springer, Berlin (2010)
62.
Jouault, F., Kurtev, I.: Transforming models with atl. In: Satellite Events at the MoDELS 2005 Conference, pp. 128–138. Springer, Berlin (2006)
63.
Klein, S., Weng, X., Frey, G., Lesage, J.J., Litz, L.: Controller design for an fms using signal interpreted petri nets and sfc: validation of both descriptions via model-checking. In: Proceedings of the 2002 American Control Conference, vol. 5, pp. 4141–4146. IEEE (2002)
64.
Klotz, T., Fordran, E., Straube, B., Haufe, J.: Formal verification of uml-modeled machine controls. In: IEEE Conference on Emerging Technologies and Factory Automation, ETFA 2009, pp. 1–7. IEEE (2009)
65.
Kornecki, A.J., Zalewski, J.: Safety and security in industrial control. In: Proceedings of the Sixth Annual Workshop on Cyber Security and Information Intelligence Research, CSIIRW ’10, pp 77:1–77:4. ACM, New York (2010). doi:10.​1145/​1852666.​1852754
66.
Kowalewski, S., Engell, S., Preußig, J., Stursberg, O.: Verification of logic controllers for continuous plants using timed condition/event-system models. Automatica 35(3), 505–518 (1999)MathSciNetCrossRefMATH
67.
Lahtinen, J.: Model checking timed safety instrumented systems. Technical report TKK-ICS-R3. Department of Computer Science, Michigan State University (2008)
68.
Lahtinen, J., Valkonen, J., Bjrkman, K., Frits, J., Niemel, I., Heljanko, K.: Model checking of safety-critical software in the nuclear engineering domain. Reliab. Eng. Syst. Saf. 105, 104–113 (2010). doi:10.​1016/​j.​ress.​2012.​03.​021, ESREL
69.
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. (STTT) 1(1), 134–152 (1997)CrossRefMATH
70.
71.
LeGuernic, P., Gautier, T., Borgne, M.L., Maire, C.L.: Programming real-time applications with signal. Proc. IEEE 79(9), 1321–1336 (1991)CrossRef
72.
Leuschel, M., Butler, M..: Prob: a model checker for b. In: FME 2003: Formal Methods, pp. 855–874. Springer (2003)
73.
74.
Lewis, R.R.W.: Programming industrial control systems using IEC 1131-3. 50, IET (1998)
75.
L’Her, D., Parc, P.L., Marcé, L.: Proving sequential function chart programs using automata. In: Automata Implementation, pp. 149–163. Springer (1999)
76.
Mader, A., Wupper, H.: Timed automaton models for simple programmable logic controllers. In: Proceedings of the 11th Euromicro Conference on Real-Time Systems, pp. 106–113. IEEE (1999)
77.
Mader, A., Brinksma, E., Wupper, H., Bauer, N.: Design of a plc control program for a batch plant vhs case study 1. Eur. J. Control 7(4), 416–439 (2001)CrossRefMATH
78.
Mazzolini, M., Brusaferri, A., Carpanzano, E.: Model-checking based verification approach for advanced industrial automation solutions. In: IEEE Conference on Emerging Technologies and Factory Automation (ETFA), pp. 1–8. IEEE (2010). doi:10.​1109/​ETFA.​2010.​5641209
79.
80.
McMillan, K.L.: The SMV Language. Cadence Berkeley Labs, Berkeley (1999)
81.
Mertke, T., Frey, G.: Formal verification of plc programs generated from signal interpreted petri nets. In: IEEE International Conference on Systems, Man, and Cybernetics, vol. 4, pp. 2700–2705. IEEE (2001)
82.
Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58–64 (2010)CrossRef
83.
84.
Moon, I.: Modeling programmable logic controllers for logic verification. IEEE Control Syst. 14(2), 53–59 (1994)CrossRef
85.
Németh, E., Bartha, T.: Formal verification of safety functions by reinterpretation of functional block based specifications. In: Cofer, D., Fantechi, A. (eds.) Formal Methods for Industrial Critical Systems, pp. 199–214. Springer (2009)
86.
Olderog, E.R.: Correct real-time software for programmable logic controllers. In: Olderog, E-R., Steffen, B. (eds.) Correct System Design, pp. 342–362. Springer, Berlin (1999)
87.
Pakonen, A., Mtsniemi, T., Lahtinen, J., Karhela, T.: A toolset for model checking of plc software. In: Proceedings of 18th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA2013 (2013)
88.
Pang, C., Vyatkin, V.: Automatic model generation of iec 61499 function block using net condition/event systems. In: 6th IEEE International Conference on Industrial Informatics, 2008. INDIN 2008, IEEE, pp 1133–1138 (2008)
89.
Pavlovic, O., Ehrich, H.D.: Model checking plc software written in function block diagram. In: Third International Conference on Software Testing, Verification and Validation (ICST), pp. 439–448 (2010). doi:10.​1109/​ICST.​2010.​10
90.
Pavlovic, O., Pinger, R., Kollmann, M.: Automated formal verification of PLC programs written in IL. In: 4th International Verification Workshop, Bremen, Germany (2007)
91.
Peleska, J., Haxthausen, A.E.: Object code verification for safety-critical railway control systems. In: Proceedings of 6th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2007), pp. 184–199 (2007)
92.
Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall PTR, Upper Saddle River (1981)MATH
93.
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS ’77. IEEE Computer Society, Washington, pp. 46–57 (1977). doi:10.​1109/​SFCS.​1977.​32
94.
Probst, S.T., Powers, G.J., Long, D., Moon, I.: Verification of a logically controlled, solids transport system using symbolic model checking. Comput. Chem. Eng. 21(4), 417–429 (1997)CrossRef
95.
Rausch, M., Krogh, B.H.: Formal verification of plc programs. In: Proceedings of the 1998 American Control Conference, vol. 1, pp. 234–238. IEEE (1998)
96.
Rossi, O., Schnoebelen, P.: Formal modeling of timed function blocks for the automatic verification of ladder diagram programs. In: Proceedings of 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems (ADPM2000), Dortmund, Germany, pp. 177–182 (2000)
97.
Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual. The Pearson Higher Education, Upper Saddle River (2004)
98.
Sacha, K.: Verification and implementation of dependable controllers. In: Third International Conference on Dependability of Computer Systems, 2008. DepCos-RELCOMEX’08, pp 143–151. IEEE (2008)
99.
Sarmento, C.A., Silva, J.R., Miyagi, P.E., Filho, D.J.S.: Modeling of programs and its verification for programmable logic controllers. In: Proceedings of IFAC 17th World Congress, pp. 10546–10551 (2008)
100.
Schlich, B., Brauer, J., Wernerus, J., Kowalewski, S.: Direct model checking of plc programs in IL. Dependable Control of Discrete Syst. 2, 28–33 (2009)
101.
Smet, O.D., Rossi, O.: Verification of a controller for a flexible manufacturing line written in ladder diagram via model-checking. In: Proceedings of the 2002 American Control Conference, 2002, vol. 5, pp. 4147–4152 (2002). doi:10.​1109/​ACC.​2002.​1024580
102.
Smet, O.D., Couffin, S., Rossi, O., Canet, G., Lesage, J., Schnoebelen, P., Papini, H.: Safe programming of plc using formal verification methods. In: Proceedings of 4th International PLCopen Conference on Industrial Control Programming (ICP’2000), Utrecht, The Netherlands, pp. 73–78 (2000)
103.
Soliman, D., Frey, G.: Verification and validation of safety applications based on PLCopen safety function blocks. Control Eng. Pract. 19(9), 929–946 (2011). doi:10.​1016/​j.​conengprac.​2011.​01.​001. special Section: DCDS09 The 2nd IFAC Workshop on Dependable Control of Discrete SystemsCrossRef
104.
Sreenivas, R.S., Krogh, B.H.: On condition/event systems with discrete state realizations. Discrete Event Dyn. Syst. 1(2), 209–236 (1991)CrossRefMATH
105.
Thapa, D., Park, J., Wang, G.N., Shin, D.: Timed-mpsg: a formal model for real-time shop floor controller. In: International Conference on Computational Intelligence for Modelling, Control and Automation, and International Conference on Intelligent Agents, pp. 101–101. Web Technologies and Internet Commerce. IEEE (2006)
106.
Turk, A.L., Probst, S.T., Powers, G.J.: Verification of real time chemical processing systems. In: Maler, O. (ed.) Hybrid and Real-Time Systems, pp. 259–272. Springer, Berlin (1997)
107.
Vulgarakis, A., Causevic, A.: Applying remes behavioral modeling to plc systems. In: XXII International Symposium on Information, Communication and Automation Technologies, ICAT 2009, pp 1–8. IEEE (2009)
108.
Vyatkin, V., Hanisch, H.M., Pfeiffer, T.: Object-oriented modular place/transition formalism for systematic modeling and validation of industrial automation systems. In: Proceedings of IEEE International Conference on Industrial Informatics, INDIN 2003, pp. 224–232. IEEE (2003)
109.
Wang, R., Song, X., Gu, M.: Modelling and verification of program logic controllers using timed automata. IET Softw. 1(4), 127–131 (2007)CrossRef
110.
Wardana, A., Folmer, J., Vogel-Heuser, B.: Automatic program verification of continuous function chart based on model checking. In: 35th Annual Conference of IEEE Industrial Electronics, IECON’09, pp. 2422–2427. IEEE (2009)
111.
Weißmann, M., Bedenk, S., Buckl, C., Knoll, A.: Model checking industrial robot systems. In: Groce, A., Musuvathi, M. (eds.) Model Checking Software, pp. 161–176. Springer, Berlin (2011)
112.
Weng, X., Litz, L.: Model checking of signal interpreted petri nets. In: IEEE International Conference on Systems, Man, and Cybernetics, vol. 4, pp. 2748–2752. IEEE (2001)
113.
Willems, H.: Compact timed automata for plc programs. Technical report CSI-R9925, University of Nijmegen, The Netherlands (1999)
114.
Witsch, D., Vogel-Heuser, B., Faure, J.M., Marsal, G.: Performance analysis of industrial ethernet networks by means of timed model-checking. In: Proceedings of the 12th IFAC Symposium on Information Control Problems in Manufacturing, INCOM 2006, Saint-Etienne, France (2006)
115.
Yoo, J., Cha, S., Jee, E.: A verification framework for fbd based software in nuclear power plants. In: 15th Asia-Pacific Software Engineering Conference, APSEC ’08, pp. 385–392 (2008). doi:10.​1109/​APSEC.​2008.​26
116.
Younis, M.B., Frey, G.: Formalization of existing plc programs: a survey. In: Proceedings of CESA, pp. 0234–0239 (2003)
117.
Yovine, S.: Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transf. (STTT) 1(1), 123–133 (1997)CrossRefMATH
118.
Zhou, M., He, F., Gu, M., Song, X. Translation-based model checking for plc programs. In: 33rd Annual IEEE International Computer Software and Applications Conference, COMPSAC ’09, vol. 1, pp. 553–562 (2009). doi:10.​1109/​COMPSAC.​2009.​80
119.
Zoubek, B., Roussel, J.M., Kwiatkowska, M.: Towards automatic verification of ladder logic programs. In: Proceedings of IMACS-IEEE’CESA’03’: Computational Engineering in Systems Applications (2003)
Metadaten
Titel
An overview of model checking practices on verification of PLC software
verfasst von
Tolga Ovatman
Atakan Aral
Davut Polat
Ali Osman Ünver
Publikationsdatum
25.12.2014
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 4/2016
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-014-0448-7

Weitere Artikel der Ausgabe 4/2016

Software and Systems Modeling 4/2016 Zur Ausgabe

Regular Paper

Supporting different process views through a Shared Process Model

Theme Section Paper

Model-checking software library API usage rules

Theme Section Paper

Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

Theme Section Paper

Knowledge-based construction of distributed constrained systems

Theme Section Paper

A formal verification framework for static analysis

Theme Section Paper

Feature Nets: behavioural modelling of software product lines