Implementing a new verification backend
- Create a plug-in project that will contain the implementation of the business logic. This plug-in will contain enough information to be directly used by the CLI.
- The plug-in should depend on
cern.plcverif.verif.interfaces
andcern.plcverif.verif.extensions
. (META-INF/MANIFEST.MF
file, Dependencies tab, Required Plug-ins field) - The plug-in should define extension for the
cern.plcverif.verif.extensions.backend
extension pointclass
: the class that will implement theIBackendExtension
interfacecmd_id
: the unique command ID that will identify this backend. For example, this ID will be used when defining the backend to be used (-job.backend=<cmd_id>
)
- Implement the
IBackendExtension
interface in a class. This factory will have to create the backend instances which will handle the verification jobs. This class should be the one set forclass
above. - Implement the
IBackend
interface in a class. The above implementation ofIBackendExtension
shall create instances of this class.getPreferredModelFormat()
should return the preferred model format, see the API documentation for more details.getPreferredRequirementFormat()
should return the preferred requirement format, see the API documentation for more details.isInliningRequired()
should return true if inlining is expected by the backend. See more about CFA inlining in the CFA instance metamodel description.areCfaAnnotationsRequired()
should return true if an annotated CFA is expected by the backend. If this is false, the annotations will be omitted from the CFA to improve the performance.- The
execute
method is the main entry point of the plug-in. When the verification job finished producing the reduced CFA of the program under verification and the requirements are available too, PLCverif will call theexecute
method with the current verification problem, the verification result object and a canceler object. The verification backend plug-in is then expected to switch to a new stage (withVerificationStageTags.BACKEND_EXECUTION
tag), obtain the result from the verification tool it represents and set it in the verification result object. More details about the responsibilities of theexecute
method can be found in its API documentation.
- The plug-in should depend on
- Typically the backend plug-ins have settings or parameters (e.g., location of the external verification tool, details of the verification, timeout). In this case, it is advised to implement the settings handling based on specific settings. More information about this and examples can be found in the general part of the documentation, as this is not specific to backend plug-ins.
If desired, create a plug-in project that will contain the GUI representation of the verification backend.
- The plug-in should depend on the previously created core plug-in, as well as on
cern.plcverif.verif.extensions.gui
. (META-INF/MANIFEST.MF
file, Dependencies tab, Required Plug-ins field) - The plug-in should define extension for the
cern.plcverif.verif.extensions.gui.part
extension point. This will represent the part of the verification case editor that corresponds to this given verification backend. The rest of the details of creating a GUI plug-in can be found in the general part of the plug-in development documentation. Here we only give an example for a dummy backend GUI extension.
Example.
public class DummyBackendGuiExtension implements IVerifGuiPartExtension { @Override public IPvGuiPart<VerificationCaseContext> createPart(Composite composite, PvDataBinding parentBinding, VerificationCaseContext context, Optional<? extends SettingsElement> installationSettings) { DummyBackendGui gui = new DummyBackendGui(context); gui.createPart(composite, parentBinding); return gui; } private class DummyBackendGui extends AbstractPvGuiPart<VerificationCaseContext> { public DummyBackendGui(VerificationCaseContext context) { super(context); } @Override public void createPart(Composite composite, PvDataBinding parentBinding) { Label label = new Label(composite, SWT.NONE); label.setText("There are no GUI settings for this plug-in."); } } }
- The plug-in should depend on the previously created core plug-in, as well as on
- If desired, it is possible to create a preference page that serves as GUI representation of the installation-specific settings of the plug-in. Check the general part of the plug-in development documentation for details and examples.