This task aims at providing methods and tools for applying deductive
tools to synchronous programs that cannot be model-checked. As
examples, the chosen synchronous language is Lustre and the deductive
proof tool is PVS.
Achieved Results:
We designed a translation tool from Lustre to PVS based on a simple
translation principle and used it to treat examples. This tool was
also made available on the web at location:
http://www.imag.fr/VERIMAG/SYNCHRONE/PVS/ so as to be used by other
partners in the project.
We designed some examples, which we felt typical of problems that
cannot be model-checked. These examples can also be found at the given
web location.
Based on these examples we made some comparison between
alternative translation methods and we launched some
study of other methods.
Conclusion:
The main lesson that can be drawn from this experiment is the
following: we initially assumed that users wanted to stay
as near as possible from their initial data-flow formalism. If
this is true, both performed translations fail in the sense that, if a
given property is not automatically proved, users have to deal with
it in the PVS language and not in the source language. This leads us
to think that the real problem is not the particular chosen
translation method, but an inverse translation allowing prover
sequents to be expressed in terms of the source language.
We therefore propose to investigate this question in the coming year.
Publications:
P. Caspi and M. Pouzet.
A co-iterative characterization of synchronous stream functions.
RR. nr. 97-07, Verimag, October 1997.
Annex A.3.4.1a