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:
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.
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.
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.
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.
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.
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).