Comparison of CFA declarations and CFA instances

It may be difficult at first glance to understand the differences between the CFA declaration (CFD) and CFA instance (CFI) metamodels. Here we show an example that highlights the key differences. The example is taken from a verification job execution, thus you may need to read the verification-specific parts of this developer documentation, especially the part about parsing STEP 7 PLC programs and the part about requirement and PLC cycle representation.

Example. The example CFD is generated by parsing the following Siemens SCL program code.

ORGANIZATION_BLOCK OB1
BEGIN
    FB1.DB1(flag := I0.0);
    FB1.DB2(flag := NOT I0.0);

    QW0 := INT_TO_WORD(DB1.out + DB2.out);
    //#ASSERT QW0 = 0
END_ORGANIZATION_BLOCK


FUNCTION_BLOCK FB1
    VAR_INPUT
        flag : BOOL;
    END_VAR
    VAR_OUTPUT
        out : INT;
    END_VAR
BEGIN
    IF flag THEN
        out := 5;
    ELSE
        out := -5;
    END_IF;
END_FUNCTION_BLOCK


DATA_BLOCK DB1 FB1   BEGIN   END_DATA_BLOCK
DATA_BLOCK DB2 FB1   BEGIN   END_DATA_BLOCK

The entry block of this program is the OB1 organization block, this will be called by the operating system cyclically. The I0.0 is an input bit address that will be handled as a non-deterministic value in each cycle. The FB1 function block defines a simple algorithm (sets the out variable to 5 or -5 depending on flag). The function block cannot be called directly, instance data blocks need to be defined which will store the internal values of the function block. Two instances are defined here: DB1 and DB2. The DB1.out and DB2.out values are independent from each other. The assertion requirement (i.e., DB1.out + DB2.out = 0) will be transformed into the structure of the automaton. The temporal logic expression to be checked is AG(__assertion_error = 0), i.e., the assertion is never violated.

CFA declaration

The STEP 7 language frontend and the assertion requirement representation plug-in will always work on the CFA declaration level. The CFD below is generated by these plug-ins for the example program code above:

CFD of the example code
Figure: CFD of the example code

The left-hand part of the graphical representation corresponds to the data structures: the defined fields and data structures. Three data structures are defined in the _global data structure, one for each automaton declaration. It would be possible to define additional data structures, for example user-defined types.

You can notice that the FB1 data structure contains a flag and an out field. However, this is just a data structure definition, these do not correspond to real instances, e.g., FB1.flag := true would not be a valid assignment in the CFA. Only the fields defined in the _global data structure (set in CfaNetworkDeclaration.rootDataStructure) are actually instantiated. Consequently, the following atomic data instances can be read or written in the automata: IX0_0 (representing I0.0), QW0, DB1.flag, DB1.out, DB2.flag, DB2.out. You can see that a "singleton" field is created for the OB1 that does not need instantiation. However, the corresponding OB1 data structure is empty. Similar singleton fields are created for functions too.

The structural part of the CFD is shown on the next figure. The structural part of the CFD

Main automaton. The VerificationLoop automaton is the main automaton of the CFD (denoted by thick border). This automaton represents the cyclic execution of the program and is created by the requirement representation plug-in. The other two automata declaration are created by the language frontend, representing the blocks in the PLC program.

Local data structures. At the top of the automata declarations, you can see their names and the corresponding local data structure definitions (e.g., VerificationLoopDS is the local data structure of the VerificationLoop automaton declaration). This data type determines the type of the expected context. The context of an automaton contains all local data elements. For example, the FB1 automaton uses the FB1 data structure as context. This defines the flag and out fields. When the FB1 automaton is called, a context needs to be provided, as the references to flag and out in this automaton are relative to the context. You can notice that the OB1 automaton declaration will call the FB1 automaton once with the DB1 context, and once with the DB2 context. The elements of the context can be accessed from other automata declarations too, but in that case relative addressing cannot be used. You can see an example for this in the OB1 automaton: DB1/out + DB2/out.

Key observations.

  • One automaton declaration is created per block, even if the block can be instantiated many times.
  • Rich data structures can be defined.
  • Only the fields directly contained by the root data structure can be written or read. The nested data structures define only a structure.
  • The CFD model is relatively close to the input language (rich data structures, instantiation).

CFA instance

The CFD model of the program code can be converted to CFA instance model (CFI) using the CfaInstantiator class. The main difference between the CFD and the CFI is the level of modeling: the CFD models the program at the level of declarations, while CFI at the level of instances. The following figure shows the CFI corresponding to the previous example.

CFI of the example code
Figure: CFI of the example code

Key observations.

  • One automaton instance is created per block instance.
  • Data structures cannot be defined. No local data structure is defined for the automata instances.
  • The CFI model is relatively simple to represent for general-purpose model checkers.

Inlined CFA instance

The CFI models may contain call transitions and several automata. However, as many verification backends do not support automata calls, during the instantiation the calls can be inlined, i.e., the calls to a given automaton can be substituted with the structure of the called automaton. (We assume the lack of recursion.)

The following figure shows the inlined version of the previous example.

Inlined CFI of the example code
Figure: Inlined CFI of the example code

Key observations.

  • There is only one automaton in the inlined CFI model (the main automaton).
  • There are no call transitions in the automaton.

The inlined CFI model is a good candidate for the automata reductions. The following figure shows the previous CFI reduced.

Inlined, reduced CFI of the example code
Figure: Inlined, reduced CFI of the example code

You can notice also that the [ELSE] guard expressions have been replaced with explicit representations, using the ElseEliminator class.

If somehow we can infer that I0.0 = false (either from a previous assignment, or the I0.0 variable is bounded to false in the verification case), even more reductions can be performed, as can be seen in the following figure.

Inlined, reduced CFI of the example code
Figure: Inlined, reduced CFI of the example code

Practically, here the complete PLC program has been reduced to the Qw0 := 0 assignment. The rest of the automaton is responsible for representing the requirement and it cannot be reduced (those elements are made frozen).

results matching ""

    No results matching ""