SYRF Project
Task 3.4: "Deductive Proofs of Data-flow Programs"
Abstract of deliverable 3.4.2
Back to the SYRF Home Page
Approach:
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 reworked the translation tool from Lustre to PVS made unavailable
because of evolutions in PVS. We propose a translation method
apparently more robust with respect to such evolutions and which seems
to correct most drawbacks of the previous one:
- it is fully functional,
- it allows the expression of multiple clocks,
- it is very close to the source Lustre language.
Conclusion:
Though not yet fully evaluated, this method looks quite appealing and
we propose to prototype it in the coming year.