• AIB 2016-07: Verification of Programmable Logic Controller Code using M

    From Jera Hensel@21:1/5 to All on Tue Nov 22 07:51:47 2016
    The following technical report is available from http://aib.informatik.rwth-aachen.de:

    Verification of Programmable Logic Controller Code using Model Checking
    and Static Analysis
    Sebastian Biallas
    AIB 2016-07

    Programmable Logic Controllers (PLCs, ger. Speicherprogrammierbare
    Steuerungen) are control devices used in industry to control, operate
    and monitor plants, machines and robots. PLCs comprise input
    connectors, typically connected to sensors, output connectors, typically connected to actuators, and a program, which controls the behavior,
    computing new output values based on the input values and an internal
    state. Since PLCs operate in safety-critical environments, where a
    malfunction could seriously harm the environment, humans, or the plant,
    it is recommended to verify their programs using formal methods.

    This dissertation studies the formal methods model checking and static
    analysis to prove the correctness of PLC programs. For this, we
    developed the tool ArcadePLC, which allows the automatic application of
    these methods to PLC programs written in different vendor-specific
    dialects. It extracts a model from the program by abstract simulation,
    which over-approximates the possible program behavior. The user is then
    able to verify whether the model obeys a specification, which can be
    written in the logic CTL or using automata.

    For applying model checking, we demonstrate how the model can be
    extracted automatically, such that the approach scales to industrial
    size programs. For this, we introduce two different abstraction
    techniques: First, we develop an abstraction refinement guided by the
    model checker that automatically creates an abstracted model by
    iteratively analyzing counterexamples. Second, we implemented a
    predicate abstraction that evaluates a formalized program semantics
    using an SMT solver. Both techniques are evaluated using different
    programs from industry and academia. Further, we introduce a simplified formalism to write specifications, which is influenced by an
    automata-based language established in industry. We implement an
    algorithm to check programs using this formalism and show that this
    technique is even able to detect errors in the specification. Finally,
    we detail how counterexamples generated by the model checker can be
    analyzed automatically to locate the actual erroneous line in the program.

    The static analysis we developed is able to detect program errors in a
    fully automatic way. We detect typical errors such as division by zero
    and illegal array accesses, but also PLC specific errors, e.g., during a restart. The analysis is based on a value-set analysis, which
    determines the values of all program variables in each program location.
    These sets are then verified against the predefined checks or
    user-provided annotations. We show how to implement this analysis such
    that it scales to industrial size programs. The approach is evaluated on
    an industrial case study.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)