
|
Verification Support Environment (VSE) |
In order to assure the highest levels of trustworthiness of software formal methods for a development of software are required. The VSE-tool was developed by a consortium of german universities and industry to make a tool available which supports this formal development process.
The VSE relies on three equally important ideas: an adequate method for programming in the large, a powerful deductive support for all formal concepts, and the integration into an administration and visualization system.
Refinement steps are specified by means of abstract programs that use concepts from the lower (import) level in order to implement the more abstract ones on the export level. The bottom layer is given by a collection of predefined concepts that can directly be realized in a target programming language. Modularity in this concext means that subspecifications can be implemented separately. At each level, safety and/or security requirements can be formulated in addition to the system specification.
The VSE-System currently runs under Allegro Common Lisp on SUN Solaris 2.5. To get more informations how you can get a copy of the system please contact:
Dieter Hutter (hutter@dfki.de) Werner Stephan (stephan@dfki.de)