[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Mon, 2 Nov 2015 14:16:08 -0800 (PST)*References*: <002a8162-9111-4725-be1f-d9e6b234db32@googlegroups.com>

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

**Follow-Ups**:**Re: Examples using Reals?***From:*Brian Beckman

**References**:**Examples using Reals?***From:*Brian Beckman

- Prev by Date:
**Re: Examples using Reals?** - Next by Date:
**2016 TLA+ Workshop** - Previous by thread:
**Re: Examples using Reals?** - Next by thread:
**Re: Examples using Reals?** - Index(es):