Automated Verification of Temporal Properties of Ladder Programs
| Autor: | Claude Marché, Denis Cousineau, David Mentré, Hiroaki Inoue, Cláudio Belo Lourenço, Florian Faissole |
|---|---|
| Přispěvatelé: | Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Mitsubishi Electric [France], Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Mitsubishi Electric Corporation, ProofInUse-MERCE |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
business.industry
Computer science Programming language Deductive verification Programmable logic controller [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering 02 engineering and technology computer.software_genre Automation Software Chart 020204 information systems Formal specification 0202 electrical engineering electronic engineering information engineering Code (cryptography) Ladder language for programming PLCs Why3 environment Timing charts Degree of confidence business computer Counterexample |
| Zdroj: | FMICS 2021-Formal Methods for Industrial Critical Systems FMICS 2021-Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩ Formal Methods for Industrial Critical Systems ISBN: 9783030852474 FMICS |
| DOI: | 10.1007/978-3-030-85248-1_2⟩ |
| Popis: | International audience; Programmable Logic Controllers (PLCs) are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop PLC software. Our aim is to prove that a given Ladder program conforms to an expected temporal behaviour given as a timing chart, describing scenarios of execution. We translate the Ladder code and the timing chart into a program for the Why3 environment, within which the verification proceeds by generating verification conditions, to be checked valid using automated theorem provers. The ultimate goal is twofold: first, by obtaining a complete proof, we can verify the conformance of the Ladder code with respect to the timing chart with a high degree of confidence. Second, when the proof is not fully completed, we obtain a counterexample, illustrating a possible execution scenario of the Ladder code which does not conform to the timing chart. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|