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

*From*: Brian Beckman <bc.be...@xxxxxxxxx>*Date*: Tue, 3 Nov 2015 10:31:31 -0800 (PST)*References*: <002a8162-9111-4725-be1f-d9e6b234db32@googlegroups.com> <9c2aff09-db56-40b8-905d-4948f9850eca@googlegroups.com>

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:

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

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

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

**Re: Examples using Reals?***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] 2016 TLA+ Workshop** - Next by Date:
**Re: Error when adding an Invariant** - Previous by thread:
**Re: Examples using Reals?** - Next by thread:
**Re: Examples using Reals?** - Index(es):