loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Nicolas Rivierre, France Telecom R&D
Francois Horn, France Telecom R&D
Fr?d?ric Dang Tran, France Telecom R&D
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.