Workplan Task D: Integrated Tool Support
Formal methods will only be used when they are supported by tools. As this
project will use a large number of methods, it is also likely that a large
number of tools will be necessary as well. This task is responsible for
developing an integrated workbench of tools, in order to avoid steep learning
curves of yet another method or yet another tool.
Ultimately, we want to develop a workbench that gives tools
-
access to other tool's data or models
-
an integrated help system
-
management facilities for versioning of models
-
management facilities for (intermediate) analysis results
The first semester activities will mainly focus on
-
getting an overview of the existing tools and methods that, in the course
of SVC, will need to be integrated. We should not try to make a comprehensive
list of all available tools, but really focus on the tools that we expect
to use the most. First, an inventory of the integration-aspects of the
tools (how open are they, do we have knowledge of the internal structure
of the tool, platform dependencies, etcetera). Then, given these aspects,
a number of tools will be analysed. A first overview of some relevant tools
are outlined in the table below:
| Univ Twente |
CWI |
TI-CO |
Other |
| LOTOS toolset |
muCRL toolset |
Testbed Tools |
Spin (Bell labs) |
|
Heer Hugo |
|
Caesar/Aldebaran |
-
An overview of requirements on the workbench level, together with an architecture
of the workbench. This workbench could borrow ideas from CWI's toolBus,
the tool-architecture used in the Testbed Project, or that of the CAESAR/Aldébaran
toolset.
Later-on during the project, work on the transformation of models from
one formalism into another, defining a common format, and defining common
functions based on that common format can start. This allows for semantic
relevant operations on the workbench-level.
Task D activities will be jointly performed by CWI, UnivTwente, and TI-CO.
This page was last updated by Holger Hermanns on
2000-03-20