DICE-Verification Tool v0.3.0

Features implemented:

• D-VerT Client (Eclipse Plugin)

  • support for Spark Models
  • new contextual launch shortcut
  • code reorganization

• D-VerT Server (Docker Multi-Container application):

  • support for Spark verification
  • improvements in TL model
  • improvements in Dashboard

Issues in progress:

• Improve transformation process from UML to JSON (so that no renaming of associations' ends is needed).
• Improve D-VerT Server Management by:
  • providing more actions to control/remove/export statistics of running tasks
  • providing single-task perspective
  • add security settings

DICE Verification Tool v0.2.0

Features implemented:

• D-VerT Client (Eclipse Plugin)
  • added default values
  • removed ae2zot from supported plugins
• D-VerT Server (Docker Multi-Container application):
  • heavy code reorganization
  • improvements in TL model

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.