DocumentCode
1995453
Title
On monitoring concurrent systems with TLA: an example
Author
Rivierre, Nicolas ; Horn, Francois ; Tran, Frédéric Dang
Author_Institution
France Telecom R&D, Issy Moulineaux, France
fYear
2005
fDate
7-9 June 2005
Firstpage
36
Lastpage
45
Abstract
We present an approach for producing oracles from TLA (temporal logic of action) 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.
Keywords
distributed processing; formal specification; storage management; system monitoring; temporal logic; Ben-Ari algorithm; TLA system specification; behavioral model; classical incremental algorithm; concurrent system monitoring; garbage collection; oracles; temporal fault detection; temporal logic of action; Algebra; Fault detection; Java; Logic functions; Logic programming; Monitoring; Research and development; Runtime; Software testing; Telecommunications;
fLanguage
English
Publisher
ieee
Conference_Titel
Application of Concurrency to System Design, 2005. ACSD 2005. Fifth International Conference on
ISSN
1550-4808
Print_ISBN
0-7695-2363-3
Type
conf
DOI
10.1109/ACSD.2005.29
Filename
1508128
Link To Document