Acções do Documento

Software

We are developing a number of tools most of which are integrated into a common framework. Software, manuals and examples will become available over the next few days. You can already download the Windows and Mac versions of the IVY workbench (click the links to download):

Integrated tool
  • IVY workbench (includes the editors, compiler and visualizer integrated through the IPF)
Individual tools
  • i2smv compiler - A compiler from MAL interactros to NuSMV
  • TraceVisualizer - An analysi tool for the traces produced by NuSMV
  • ModelsEditor - A graphical editor for MAL interactors
  • PropertiesEditor - An editor of properties for model checking
  • AniMAL - An animator of MAL interactor models
  • IPF (Interactors Plugin Framework) - The framework that brings all of the above together
  • GUIsurfer - A reverse engineering tool for user interface code
  • TOM (Task to Oracles Mapping tool) - a tool that generates Spec# oracles from CTT models (for testing with Spec Explorer)
Manuals
  • Soon...
Models
  • A/C System - model used in the DSV-IS 2008 paper: Systematic analysis of control panel interfaces using formal tools (Campos and Harrison)
  • for more see HCIspecs...