DICE Verification Tool v0.1.0

Initial release of the DICE Verification Tool (D-VerT).

Features implemented:

• D-VerT Client (Eclipse Plugin)
  • Support for Storm topologies described as Papyrus UML Class diagrams annotated with the DICE:Storm:DTSM profile.
  • Automatic transformation from DICE-profiled UML diagrams to an intermediate JSON format, to be provided to D-VerT Server.
  • Invocation of D-VerT Server to launch verification tasks on the designed application.
  • Visualization of D-VerT Server Dashboard from a Browser view in the DICE IDE.
  • Configuration of connection to server from preference page (Setting default values) and from launch configuration page.
• D-VerT Server (Docker Multi-Container application):
  • Flask application that makes use of Celery task queue to manage long running verification tasks and persists task status and results on Redis backend.
  • Launch verification tasks of Storm topologies specified as JSON objects by:
    • generating a .lisp file containing the corresponding temporal logic model
    • providing the .lisp file to the Zot formal verification tool
  • Results and status of the running tasks are visible from the DVerT Server Dashboard reachable at <server-host-address>:5000.