Ladder Metamodeling & PLC Program Validation through Time Petri NetsReportar como inadecuado

Ladder Metamodeling & PLC Program Validation through Time Petri Nets - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 IRIT - Institut de recherche en informatique de Toulouse 2 Federal University of Santa Catarina 3 LAAS - Laboratoire d-analyse et d-architecture des systèmes Toulouse

Abstract : Ladder Diagram LD is the most used programming language for Programmable Logical Controllers PLCs. A PLC is a special purpose industrial computer used to automate industrial processes. Bugs in LD programs are very costly and sometimes are even a threat to human safety. We propose a model driven approach for formal verification of LD programs through model-checking. We provide a metamodel for a subset of the LD language. We define a time Petri net TPN semantics for LD programs through an ATL model transformation. Finally, we automatically generate behavioral properties over the LD models as LTL formulae which are then checked over the generated TPN using the model-checkers available in the Tina toolkit. We focus on race condition detection. This work is supported by the topcased project, part of the french cluster Aerospace Valley granted by the french DGE, cf.

keyword : MDA Time Petri Nets PLC Ladder Diagram Formal Verification Model Checking Model Transformation ATL

Autor: Darlam Bender - Benoît Combemale - Xavier Crégut - Jean-Marie Farines - Bernard Berthomieu - François Vernadat -



Documentos relacionados