On monitoring concurrent systems with TLA: an example
- Resource Type
- Conference
- Authors
- Rivierre, N.; Horn, F.; Tran, F.D.
- Source
- Fifth International Conference on Application of Concurrency to System Design (ACSD'05) Concurrency to system design Application of Concurrency to System Design, 2005. ACSD 2005. Fifth International Conference on. :36-45 2005
- Subject
- Computing and Processing
Monitoring
Runtime
Java
Software testing
Telecommunications
Research and development
Fault detection
Logic functions
Logic programming
Algebra
- Language
- ISSN
- 1550-4808
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.