Skip to main content
Erschienen in:

01.11.2022 | General

Automated formal analysis of temporal properties of Ladder programs

verfasst von: Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 6/2022

Einloggen

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

search-config
loading …

Abstract

Programmable Logic Controllers are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop software for such controllers. In this work, we consider the description of the expected behaviour of a Ladder program under the form of a timing chart, describing a scenario of execution. Our aim is to prove that the given Ladder program conforms to the expected temporal behaviour given by such a timing chart. Our approach amounts to translating the Ladder code, together with the timing chart, into a program for the Why3 environment for deductive program verification. The verification proceeds with the generation of verification conditions: mathematical formulas to be checked valid using automated theorem provers. The ultimate goal is twofold. On the one hand, by obtaining a complete proof, one verifies the conformity of the Ladder code with respect to the timing chart with a high degree of confidence. On the other hand, in the case the proof is not fully completed, one obtains a counterexample, illustrating a possible execution scenario of the Ladder code which does not conform to the timing chart.

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!

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!

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!

Fußnoten
1
There are no true do-while loops in WhyML, we just mean by do-while style loop a piece of code of the form “ https://static-content.springer.com/image/art%3A10.1007%2Fs10009-022-00680-0/MediaObjects/10009_2022_680_Figy_HTML.gif ” with two occurrences of the loop body.
 
Literatur
6.
Zurück zum Zitat Biallas, S., Kowalewski, S., Stattelmann, S., Schlich, B.: Efficient handling of states in abstract interpretation of industrial programmable logic controller code. In: 12th international workshop on discrete event systems, pp. 400–405. IFAC (2014) Biallas, S., Kowalewski, S., Stattelmann, S., Schlich, B.: Efficient handling of states in abstract interpretation of industrial programmable logic controller code. In: 12th international workshop on discrete event systems, pp. 400–405. IFAC (2014)
7.
Zurück zum Zitat Bobot, F, Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie–first international workshop on intermediate verification languages, pp. 53–64. http://hal.inria.fr/hal-00790310 (2011) Bobot, F, Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie–first international workshop on intermediate verification languages, pp. 53–64. http://​hal.​inria.​fr/​hal-00790310 (2011)
11.
Zurück zum Zitat Cousineau, D., Mentré, D., Inoue, H.: Automated deductive verification for ladder programming. In: F-IDE–fifth workshop on formal integrated development environments. Electronic Proceedings in Theoretical Computer Science, vol. 310, pp. 7–12. (2019) https://doi.org/10.4204/EPTCS.310.2 Cousineau, D., Mentré, D., Inoue, H.: Automated deductive verification for ladder programming. In: F-IDE–fifth workshop on formal integrated development environments. Electronic Proceedings in Theoretical Computer Science, vol. 310, pp. 7–12. (2019) https://​doi.​org/​10.​4204/​EPTCS.​310.​2
17.
Zurück zum Zitat Fehnker, A., Huuck, R., Schlich, B., Tapp, M.: Automatic bug detection in microcontroller software by static program analysis. In: SOFSEM – theory and practice of computer science. Lecture Notes in Computer Science, vol. 5404, pp. 267–278. Springer (2009) https://doi.org/10.1007/978-3-540-95891-8_26 Fehnker, A., Huuck, R., Schlich, B., Tapp, M.: Automatic bug detection in microcontroller software by static program analysis. In: SOFSEM – theory and practice of computer science. Lecture Notes in Computer Science, vol. 5404, pp. 267–278. Springer (2009) https://​doi.​org/​10.​1007/​978-3-540-95891-8_​26
19.
Zurück zum Zitat Filliâtre, J.-C., Paskevich, A.: Why3–where programs meet provers. In: ESOP–22nd European symposium on programming. Lecture Notes in Computer Science, vol. 7792, pp. 125–128. Springer (2013) http://hal.inria.fr/hal-00789533 Filliâtre, J.-C., Paskevich, A.: Why3–where programs meet provers. In: ESOP–22nd European symposium on programming. Lecture Notes in Computer Science, vol. 7792, pp. 125–128. Springer (2013) http://​hal.​inria.​fr/​hal-00789533
21.
Zurück zum Zitat Jeannet, Bertrand, Miné, Antoine: Apron: A library of numerical abstract domains for static analysis. In CAV – Computer Aided Verification, pages 661–667. Springer (2009) Jeannet, Bertrand, Miné, Antoine: Apron: A library of numerical abstract domains for static analysis. In CAV – Computer Aided Verification, pages 661–667. Springer (2009)
23.
Zurück zum Zitat John, W., McCormick, Peter, C.: Building High Integrity Applications with SPARK. Cambridge University Press, Chapin (2015) John, W., McCormick, Peter, C.: Building High Integrity Applications with SPARK. Cambridge University Press, Chapin (2015)
Metadaten
Titel
Automated formal analysis of temporal properties of Ladder programs
verfasst von
Cláudio Belo Lourenço
Denis Cousineau
Florian Faissole
Claude Marché
David Mentré
Hiroaki Inoue
Publikationsdatum
01.11.2022
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 6/2022
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00680-0

Weitere Artikel der Ausgabe 6/2022

International Journal on Software Tools for Technology Transfer 6/2022 Zur Ausgabe

Premium Partner