Abstract
Methods for mechanically synthesizing concurrent programs from temporal logic specifications obviate the need to manually construct a program and compose a proof of its correctness. A serious drawback of extant synthesis methods, however, is that they produce concurrent programs for models of computation that are often unrealistic. In particular, these methods assume completely fault-free operation, that is, the programs they produce are fault-intolerant. In this paper, we show how to mechanically synthesize fault-tolerant concurrent programs for various fault classes. We illustrate our method by synthesizing fault-tolerant solutions to the mutual exclusion and barrier synchronization problems.
Original language | English (US) |
---|---|
Pages (from-to) | 125-185 |
Number of pages | 61 |
Journal | ACM Transactions on Programming Languages and Systems |
Volume | 26 |
Issue number | 1 |
DOIs | |
State | Published - Jan 2004 |
Externally published | Yes |
Keywords
- Concurrent programs
- Fault-tolerance
- Program synthesis
- Specification
- Temporal logic
ASJC Scopus subject areas
- Software