Verification job

As it was previously discussed, PLCverif provides a generic job interface that can be used for implementing any workflow that is based on parsed CFAs of PLC programs. However, the main goal of PLCverif is to provide formal verification (model checking) for PLC programs. Thus the verification job that is shipped with PLCverif has utmost importance.

A verification job takes a PLC code and a requirement. It represents the PLC code as CFA, the CFA will be reduced, the represented formal requirement will be checked on the CFA by a verification backend. The results will be made available by reporters. This section overviews the workflow implemented by the verification job and the key data structures used in it.

Verification workflow

The workflow implemented by the verification job (in VerificationJob.execute()) is summarized on the following figure.

The following sequence diagram gives a more detailed overview of the steps.

Verification metamodel

The following figure overviews the data structures used by the verification job.

• The VerificationJob class implements the verification workflow and orchestrates each of its steps
  • It extends the AbstractBasicJob abstract class, implements the ICfaJob interface
  • It relies on three types of extensions: requirement represented (exactly one), verification backend (exactly one), and reporters (zero or more). In addition, it relies on the more generic extensions defined by the platform and provided in the ModelTasks instance: the parser or language frontend (exactly one) and CFA reductions (zero or more). Details can be found below.
  • It is instantiated by the VerificationJobExtension factory class
• The VerificationProblem represents the verification (model checking) problem (model and requirement) for the verification backend.
• The VerificationResult aggregates the results of the steps of the verification job.
  • It inherits from JobResult and transitively from the BasicJobResult abstract classes. See more details about them in their documentation
  • Read more details below
• The VerificationSettings stores the settings relevant to the verification job in a parsed form.
  • Read more details below

Verification problem (VerificationProblem)

The verification problem defines the inputs of the verification backend. It contains the model (CFA declaration or instance network) that needs to be represented by the verification backend, the temporal logic requirement (and its representation strategy), and certain additional useful information about the model (the end of cycle location, the entry context, etc.).

See more details in the API documentation.

Verification result (VerificationResult)

The verification result aggregates the results of the operations related to the verification job. It extends the JobResult class.

Further included data:

• The original main automaton of the parsed CfaNetworkDeclaration model (see getOriginalMainAutomaton())
• The original main context of the parsed CfaNetworkDeclaration model (see getOriginalMainContext())
• An Expression describing the requirement using DataRef references (see getDeclarationRequirement())
• An Expression describing the requirement using AbstractVariableRef references (see getInstanceRequirement())
• A set of additional variables introduced by the IRequirement or other plugins (see getAdditionalVariables())
• The list of fields treated as inputs (see getInputFields())
• The list of fields treated as parameters (see getParamFields())
• Map representing the field-value binding (see getBindings())
• The name of the IBackend (see getBackendName())
• The potential size of the state space (see getPotentialStateSpaceSize())
• The potential counterexample using DataRef instances (see getDeclarationCounterexample())
• The potential counterexample using AbstractVariableRef instances (see getInstanceCounterexample())
• The result of the verification (see getResult())

VerificationResult extends JobResult, thus it also stores the properties defined for the job result.

Notes:

• If the instanceCounterexample is set and the variableTrace is available, the declarationCounterexample will be created automatically.

See more details in the API documentation.

Components of verification

The verification-specific extensions are defined in cern.plcverif.verif.interfaces.

The connection between the verification job and the different extensions is shown on the following figure.

Language frontend

The language frontend is responsible for parsing the input PLC program. This is a generic platform extension, thus more details can be found in the description of the platform extensions.

Reductions

The CFA reductions are responsible for simplify and reduce the CFA representations of the parsed programs. This is a generic platform extension, thus more details can be found in the description of the platform extensions.

Requirement

A requirement should provide a way to specify formal properties subject to verification. It is also responsible for generating the full VerificationProblem. Furthermore, the requirement can provide additional diagnosis once the verification engine has been executed and the verification results are available.

See more details in the API documentation of IRequirement.

[info] More information

PLCverif is shipped with several requirement representation extensions. See the library documentation to find more information about the built-in requirements.

Verification backend

A verification backend is a component that performs the formal verification of a requirement on a CFA model (possible with the help of an external tool), also parsing the results of the analysis. They are typically wrappers of external model checker tools, but it is also possible to implement a custom model checking algorithm as a verification backend extension.

This extension is responsible to solve the verification problem (VerificationProblem) that represents a formal verification problem, specifying the model and the property to check.

See more details in the API documentation of IBackend.

[info] More information

PLCverif is shipped with several verification backend extensions. See the library documentation to find more information about the built-in verification backends.

Verification reporter

A verification reporter is a component that transforms a VerificationProblem into some other artifact that can serve as a processable report.

A reporter may log to the console but should not create files, as it is up to the client code invoking the job to decide what to do with the generated artifacts (it is possible that the results are only displayed in a window). Any artifact that is supposed to be persisted should be added to the result itself in JobResult.addFileToSave() by specifying the desired relative file path (relative to the specified output directory) and the content of the file.

See more details in the API documentation of IVerificationReporter.

[info] More information

See the library documentation to find more information about the built-in verification reporters.

Counterexample representation

The verification result can store a counterexample (or witness). Two different class structure exist for representing counterexamples, depending on whether it is a counterexample on a CFA instance or on a CFA declaration. The two class structures are very similar.

• The root object of a counterexample is a DeclarationCounterexample or InstanceCounterexample that represents a full counterexample (or witness)
• The counterexample consists of steps (DeclarationCexStep or InstanceCexStep). These are consecutive sequential steps in the counterexample. A step is expected to correspond to a PLC cycle. Each step can be named.
• Each step contains a collection of variable-value pairs (DeclarationCexStep.VariableValuePair, InstanceCounterexample.VariableValuePair). The variable in those pairs need to be a reference to a variable in the CFA declaration (i.e., a DataRef) or in the CFA instance (i.e., a AbstractVariableRef). The value shall be a literal in both cases.

[info] Automated generation of declaration counterexample

If the variable trace generated during the instantiation of the CFA declaration is available, the verification result object will take care of automatically generating the declaration counterexample based on the instance counterexample. Therefore it can be expected that the declaration counterexample is always available, no matter if the chosen backend uses CFA declaration or CFA instance models.

Verification job settings

The verification job plug-in can be configured using PLCverif settings (typically with the prefix job.) which will partially be represented by a VerificationJobSettings instance. The rest of the settings will be parsed by the VerificationJobExtension and directly handed over to the VerificationJob.