|
||
  |
release 1.0date: 4/16/2004 |
|
1. Description
VICS,
Verification of an Implementation Conforming to its Specification,
aims to
check (i.e. not to prove) the correctness of a
refinement of the B formal method, between an abstract machine
(a formal specification) and its possible implementation [
B Site pages,
B-Book].
This tool is based on
Mozart.
The context of use of this tool is essentially academic. This tool
can be used for programming courses: the
correct abstract machine is given by the teacher
and the student has to write the corresponding implementation
(in B0, a pascal like syntax). The students use this tool to
check if their implementations are correct. If not, VICS gives
a counter-example.
This project has been proposed on Sourceforge because it needs people
to contribute to the development and the documentation.
Functionalites
- basic edition of abstract machines and implementations,
- basic syntax parsing of abstract machines and implementations (for the subset of the B language VICS supports),
-
refinement checking:
- gives one counter example if the refinement is not verified,
- syntax colouring (identifiers and constraints)
Origin
This project was asked by professor
Pierre-Yves Schobbens
(FUNDP, Belgium).
VICS has been parlty realized by Laïka Moussa during
her work experience placement at
CETIC,
under the direction of Pierre-Yves Schobbens and
Emmanuel Dieul.
VICS took advantage of
Isabelle Dony
's work.
More informations can be found (in french) at
www.cetic.be/article78.html
(report on the conception).
Emmanuel Dieul has mainly developed the first public release
of VICS.
This tool was presented at:
Documentation
No documentation is available at the moment, but some could be found
in french at
www.cetic.be/article78.html.
2. Downloads
| release 1.0 4/16/2004 |
First release
Sources :
|