TLC and RealTime

[Chris Pacejo]

Hi all, dumb question: Given that TLC does not support temporal existential quantification, and that the RTBound operator is defined using a temporal existential quantifier, what is the expected way to check real-time properties with TLC?

Should I take RealTime as a template and manually incorporate its ideas into my own spec without using temporal existential quantification? (This seems to be the approach taken by the MCRealTimeHourClock example in the distribution, but it is labeled "Random junk right now" so I don't know how much attention I should pay it.)

For context, I am specifying a simple algorithm where certain steps may take real time, and I want to ensure that the whole algorithm completes within some real time bound.

[Leslie Lamport]

I have never had occasion to write a practical real-time
specification, so I can't say what really works.  Often, engineers
think they need to use real time because their system uses timeouts.
However, in most of today's distributed systems, timeouts are used
only to ensure some liveness property.  In that case, a timeout can be
modeled as an action that can be (but need not be) taken at any time.
If you really need to check that some actions happen within some
specific length of time, them you need real-time specification.

The method described in "Specifying Systems" might work for proofs,
but it's not for model checking.  I wrote a paper called "Real Time is
Really Simple" with a method for model checking real-time properties.
The non-obvious part of that paper probably doesn't apply to what
you're doing, since checking your spec over a fixed time period is
probably good enough.  You can find the paper and a discussion of it at

   http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#real-simple

Leslie

[Chris Pacejo]

Hi Leslie, thanks for the quick reply.  I believe our case is one which would benefit from true real-time checking.  Briefly, we have two classes of real-time constraints: those which arise from end-user requirements (e.g. a data processing rate or latency guarantee); and those which arise from internal communication (e.g., ensure systems A and B do not livelock due to incompatible timeouts).  Otherwise I agree that simply modeling timeouts as an optional action would suffice.

I did see "Real Time is Really Simple" but did not realize it was detailing a different method than the RealTime module uses.  I will give it a read this weekend, thanks!

- Chris