ProMoVer

Usage

In this page we explain the usage of ProMoVer web interface. The web interface is only designed to give users the opportunity to try ProMoVer. A complete full-fledged tool release is in our future plans.

• Configurations
• In Library of Global Properties section you can find our library of pre-defined global property.
• In Public Methods and Inlining section you can choose to specify all methods or public methods only. If you choose to specify public methods only, the method graph of private methods are inlined into the method graphs of public methods and then the verification is performed.
• In Property Specification Language section you can choose the specification language you want to use. For definition and syntax of the specification languages, please read our publications. If you want to use Safety-LTL, please check our tips for using safety-LTL logic as well.
  The modal equation system specification language is intended to be used when the specifications which are generated by specification extractor are inspected and refined by the user and then inserted into the program annotations. By selecting this option, the local model checking is by passed.
• Annotation Tags

• @global_interface:

  is used to specify the global interface of the program. The global interface is supposed to include all methods that are provided by the class.

• @global_ltl_prop:

  is used to specify the global property in safety-LTL language.

• @local_interface:

  is used to specify the local interface of a method. The local interface of a method is supposed to include all methods that are required by the method.

• @local_ltl_prop:

  is used to specify the local property of a method in safety-LTL language.

• @local_sl_prop:

  is used to specify the local property of a method in simulation logic language.

• @local_eq_prop:

  is used to specify the local property of a method in modal equation system language.


• Program Verification
• Simply paste your annotated Java class in the Program textarea.
  • Notice that the annotated Java class has to be compilable with JDK1.6.0, and it should not need any special class path or package.
  • The program should have a main method that creates an instance of the class and calls the first method of the class by the created instance.
  • The class should be public.
• Write the class name in the textbox Class Name
• Push the Verify button, to verify you annotated Java program.
• Buttons
• By pushing Prove By Extract Spec. button, the program is proved based on the specifications automatically extracted from the program's code. When you are using this feature, the methods need not to be specified but you need to specify the global property of the whole program. This feature provides a completely automatic verification of programs.
• By pushing Extract Spec. button, the specification of methods of the program are extracted and printed out. User can inspect the extracted specifications and remove unnecessary order of method invocations and use these specifications for verifying program.
• ProMoVer web interface provides proof storage and reuse mechanism. To provide this feature by ProMoVer web interface we need to define user accounts and assign disk quota for the users which is not yet possible for us due to the lack of facilities. Therefore, just to demonstrate the abilities of the proof storage and reuse mechanism, we provide short-term memory for users to be able to store their proofs and reuse them. The short-term memory will be deleted by terminating the session.
  By pushing Delete Previous Proofs button, you can delete the stored proofs of your program.

The verification result is shown after some time. Notice that the result may take some minutes to appear.