[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
about proving liveness and termination using PVS
Dear PVS users.
I've started using PVS recently. I want to prove some
liveness properties of LUSTRE(data-flow language)-like models.
I am aware that Dr Caspi and his colleages wrote some papers
on this topic, but they dealt with only safety properties,
as far as I am concerned.
I think the problem is related to the proof of termination
using well-foundedness. (Liveness proof using fairness
is not relevant, because the behavior is synchronous to
a common clock.) I know it is a relatively old topic,
but I couldn't find references dealing with this kind of problem
- using PVS to prove termination (or liveness) with well-foundedness.
If anyone knows some materials on it, please tell me.
Seung Mo Cho.