The Frama-PLC tool performs syntactical and semantic checks of PLC application software (developed with Control Expert by Schneider Electric - tool renamed into EcoStruxure) in relying on Frama-C platform. The tool is operational and can be considered as an advanced prototype able to analyse ZEF development files (Application exchange files proposed by Schneider Electrics tool). It supports most of the constructs of the Ladder Diagrams (LD), Sequential Function Charts (SFC) and Structured Text (ST) languages.

Further Reading

The syntactical checks are reported during the first analysis step of Frama-PLC whereas the semantic checks are reported during the second step what uses EVA and WP plugins of Frama-C. A viewer tool can be used to navigates into the reported checks and classifies them.

Online Documentation: