English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Programmable Logic Controllers (PLC) and its programming standard IEC 61131-3are widely used in embedded systems for the industrial automation domain. Wepropose a framework for the formal treatment of PLC based on the IEC 61131-3standard. A PLC system description typically combines code written in differentlanguages that are defined in IEC 61131-3. For the top-level specification weregard the Sequential Function Charts (SFC) language, a graphical high-levellanguage that allows to describe the main control-flow of the system. Inaddition to this, we describe the Instruction List (IL) language -- an assemblylike language -- and two other graphical languages: Ladder Diagrams (LD) andFunction Block Diagrams (FBD). IL, LD, and FBD are used to describe more lowlevel structures of a PLC. We formalize the semantics of these languages anddescribe and prove relations between them. Formalization and associated proofsare carried out using the proof assistant Coq. In addition to this, we presentwork on a tool for automatically generating SFC representations from agraphical description -- the IL and LD languages can be handled in Coq directly-- and its usage for verification purposes. We sketch possible usages of ourformal framework, and present an example application for a PLC in a projectdemonstrator and prove safety properties.

On Formal Reasoning on the Semantics of PLC using Coq