Implementing a new verification backend

  1. 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 and cern.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 point
      • class: the class that will implement the IBackendExtension interface
      • cmd_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 for class above.
    • Implement the IBackend interface in a class. The above implementation of IBackendExtension 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 the execute 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 (with VerificationStageTags.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 the execute method can be found in its API documentation.
  2. 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.
  3. 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.");
                 }
             }
         }
      
  4. 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.

results matching ""

    No results matching ""