On Monitoring Concurrent Systems with TLA: An Example

St. Malo, France June 07-June 09

DOI Bookmark:

http://doi.ieeecomputersociety.org/10.1109/ACSD.2005.29

Fifth International Conference on App ...

	This Article
	PURCHASE ARTICLE: $19 PDF HTML IEEE Xplore Subscribers
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Nicolas Rivierre Articles by Francois Horn Articles by Fr?d?ric Dang Tran

	ASCII Text	x
	Nicolas Rivierre, Francois Horn, Fr?d?ric Dang Tran, "On Monitoring Concurrent Systems with TLA: An Example," Application of Concurrency to System Design, International Conference on, pp. 36-45, Fifth International Conference on Application of Concurrency to System Design (ACSD'05), 2005.

	BibTex	x
	@article{ 10.1109/ACSD.2005.29, author = {Nicolas Rivierre and Francois Horn and Fr?d?ric Dang Tran}, title = {On Monitoring Concurrent Systems with TLA: An Example}, journal ={Application of Concurrency to System Design, International Conference on}, volume = {0}, year = {2005}, issn = {1550-4808}, pages = {36-45}, doi = {http://doi.ieeecomputersociety.org/10.1109/ACSD.2005.29}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Application of Concurrency to System Design, International Conference on TI - On Monitoring Concurrent Systems with TLA: An Example SN - 1550-4808 SP36 EP45 A1 - Nicolas Rivierre, A1 - Francois Horn, A1 - Fr?d?ric Dang Tran, PY - 2005 KW - null VL - 0 JA - Application of Concurrency to System Design, International Conference on ER -

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

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.