Fifth International Conference on Application of Concurrency to System Design (ACSD'05)
On Monitoring Concurrent Systems with TLA: An Example
St. Malo, France
June 07-June 09
ISBN: 0-7695-2363-3
We present an approach for producing oracles from TLA specification of a system. Such oracles are useful, for monitoring purposes, to detect temporal faults by checking a running implementation of a system against a verified behavioral model. We use the Ben-Ari classical incremental garbage collection algorithm for illustration.
Citation:
Nicolas Rivierre, Francois Horn, Fr?d?ric Dang Tran, "On Monitoring Concurrent Systems with TLA: An Example," acsd, pp.36-45, Fifth International Conference on Application of Concurrency to System Design (ACSD'05), 2005