Tools page

From Wiki.overturetool.org

Jump to: navigation, search

Overall Tool Strategic Considerations

From a strategic perspective it is important to be able to use the Overture tool both for serious work using different VDM dialects as well as for experimentation purposes for new features and/or language adjustments. Thus, it is necessary both to have a series of stable releases which are produced with regular intervals on a main branch of the development and in addition also to have experimental branches where research projects and students can experiment in different ways. When the community agrees upon the value of such new experimental features or language adjustments (see the Language Board) are worthwhile they can be moved over to the main branch.

The existing Overture tool is weakest with respect to its ability for general verification features and thus adding support for model checking and proof support is one of the prime extensive targets for the next 5 years.

Some Project Topics

  • Incorporation of GUI and basic checks already present on the Eclipse platform. Since Overture is developed on top of the Eclipse platform it is essential to make use of the features already supported on that platform. This includes syntax highlighted editors, literate programming support, easy browsing of large models and re-factoring support.
  • Automation of tests derived from VDM models using different principles.
  • Validation overview support in the form of test coverage (both statement and branch coverage), visualisation of executions in different graphical forms and general test automation support in different forms.
  • Linking of the VDM interpreters with models written in different other notations. This include the combination of the VDM-RT interpreter with continuous time simulators such as 20Sim or Simulink as it is currently being made in the DESTECS project.
  • Mixed-mode discharging of proof obligations (POs). POs can be automatically generated from VDM++ models and Sander Vermolen's project has shown that many can be automatically discharged by a HOL-based prover. Some, of course, can not and for these it might be appropriate to generate tests. This is an instance of the general problem of discharging some lemmas in proofs. In cases where automatic proof of proof obligations is not possible it may be very interesting in gaining a higher level of confidence by generating tests from the POs in question.
  • Connection to different standard development environments and notations. This includes code generators and potential combinations with databases. Also issues such as reverse engineering support, generators of GUI applications and connection to graphical notations such as UML2 (prototype already available), AADL and SysML can be envisaged here.
Retrieved from "http://wiki.overturetool.org/index.php/Tools_page"