[tlaplus] Checking Real Time Systems and TLA+

[Felipe Lisboa <lisboafelipe5@xxxxxxxxx>]

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.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e7ae930d-a125-486b-89f4-4f6c2eb9835dn%40googlegroups.com.