Methods+Apps page

From Wiki.overturetool.org

Jump to: navigation, search

Methods and Applications

The purpose of work in this strand is to develop a body of knowledge about the application of VDM and its tools. This will include records of practical experience in constructing and analysing models, modelling patterns and guidelines, and models associated with specific challenge problems.


Challenge Problems

The challenge problems is to provide a benchmark for VDM technology against our goals and, to a limited extent, provide a basis for comparison with other formalisms and tool sets.

  • Pacemaker: The Pacemaker challenge has been used as a way of trialling the methodology for model development in distributed real-time systems.
  • Verifiable (posix) file store: identify a potential contribution area.
  • Mondex: use this as a basis for involving more people in the research community. Provide a benchamrking against the state of the art by conducting some sample formal proofs (by hand and using Sander's tools), doing illustrative testing and API-based validation work.
Retrieved from "http://wiki.overturetool.org/index.php/Methods%2BApps_page"
Personal tools