I'm analyzing some designs written by other people, and trying to encode them
in TLA to get the benefits of precision and checkability.
The designers of the systems I'm analyzing write things that look a little like
Mealy machines, except they have "rich" rules such as "if the system stays
in state A for more than 2 minutes, make a transition to state B." I may be able
to model these, as you say, as "... asynchronous events unrelated to time with
... fairness conditions to ensure that a timeout eventually happens ..." I will
try that approach.
I will also look for your paper on embedded systems.
On Monday, November 2, 2015 at 2:16:09 PM UTC-8, Leslie Lamport wrote:
A sensible model of a system that uses real time will not depend on continuity properties of the reals. Hence, systems can be modeled with time assuming integer values. Whether model checking can be effective at catching errors in such specs is a question I can't answer because I have no experience with industrial systems that make use of real time. Except in embedded systems, real-time is generally used only for timeouts and can be modeled by letting timeout be an asynchronous event unrelated to time, since it's dangerous to rely on timeout values for correctness. (Fairness conditions can be used to ensure that a timeout eventually happens if a desired action doesn't occur.) For embedded systems, you might want to look at a paper I wrote called something like "Real Time is Really Simple".
Leslie