[tlaplus] Re: Checking Real Time Systems and TLA+

Answering questions 1 and 4: If you read the model checking section in Real Time is Really Simple, you'll see Leslie used VIEW to remove the global clock from the model. This stopped the state from increasing monotonically and so the state space became finite. If at all possible, try to specify your system so that it only depends on relative time (for example using upper- and lower-bound timers) rather than absolute time. If you do this, you can either use VIEW to remove your global clock variable, or just omit it from the spec entirely. I've found that TLC works quite well when modelchecking my realtime system written in this way, but there are so many parameters affecting model checking time it is difficult to give a general answer. Writing your spec this way also makes it feasible to check temporal properties, which otherwise interact poorly with state or action constraints.

On Friday, February 26, 2021 at 9:16:18 AM UTC-5 lisboa...@xxxxxxxxx wrote:

I am writing the spec of a DRAM controller on TLA+. It is a processor-level real-time system. The controller sends a series of different commands to the DRAM. These commands have to respect interval lower bounds between themselves. The system also has arrival dates, deadlines and other scheduling concepts in it.
In the first place, I wrote the spec with an explicit variable representing clock cycles. That worked fine, but the state space exploded, and the time for running TLC as well. Than, after reading some works [1], [2] and [3], I changed my approach to something like specified in the module RealTimeNew [3]. Still, I have some key questions about proving time constraints with TLA+.

1. Concerning low level RT systems, how feasible is to use TLA+ with a variable being incremented by the unit ? Is this a common practice ? Or people usually recur more often to use more low-level hardware oriented languages ? My concerns are related to performance.

2. Can we check temporal properties of this type : "Does an action happen before this variable reach such value" ?

3. (For anyone who ever worked with RealTimeNew [3]) Does the module decribed in the paper have an official code ? It's only partially described in [3]. If someone does have familiarity with it, there is a definition for IntervalBound(), which specifies a bound for the interval between two actions, but this interval is described by all the actions that can possibly happen in between (or that must happen, didn't quite get it). But that would only make it useful for describing sequential programs, in my opinion. Does anyone have a real use case of that module ?

4. How is the termination of RT systems (which often produce infinite behaviors) modelled in TLA+ ? People just check it untill a certain moment of time and say it's good enough ?

Ref

[1] Lamport, Leslie. "Real time is really simple." Microsoft Research (2005): 2005-30.

[2] Lamport, Leslie. "Real-time model checking is really simple." Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Springer, Berlin, Heidelberg, 2005.

[3] Zhang, Hehua, Ming Gu, and Xiaoyu Song. "Specifying time-sensitive systems with TLA+." 2010 IEEE 34th Annual Computer Software and Applications Conference. IEEE, 2010.