Hi Marc,
I would really love to see more documentation on "6c. Real-time and
hybrid specs"... Still I would like to know how an engineer without
the knowledge or time to do formal proofs could use TLA+ for this kind
of problems. What are the limits? or do you think that an engineer
facing this kind of problems should learn formal proofs?
First of all, even if you don't check it, writing a spec helps you
understand what you're doing. And TLA+ is a good language for writing
such a spec.
For real-time specs, I have two suggestions:
1. Try to avoid the real-time aspects. A typical use of time is for
timeouts. If that's all time is being used for, then replace actions
that happen on a timeout by actions that can occur any time. Most
uses of timeout are to assure liveness properties--safety properties
shouldn't depend on choosing the right value for when the timeout
occurs.
2. Try using discrete instead of continuous time. Correctness of the
system shouldn't depend on having continuous time rather than time
that advances every femtosecond. The Charme paper you mention describes
how such a spec can be written and model checked. (The longer paper
from which that paper was abstracted might be a better place to look.)
I'm pretty sure this method can work for toy problems. I don't know
how well it will work on a real industrial problem.
For hybrid specs, the real world is generally modeled with physical
laws based on continuous time. It may be possible to use approach 2,
modeling the physical processes with discrete (probably linear)
worst-case approximations. It would be a good exercise (possibly even
publishable) to see if this works on a toy example like the gas-burner.
(Search for "burner" on my publications page.) I don't have the time
to do it myself.
I'm also pretty curious about what can you write about "8. Something
about writing informal specs." :)
Me too.
Leslie