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
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ACSD.2005.29
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 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||