Synthesis of Fault-Tolerant Concurrent Programs (Extended Abstract)

) Anish ARORA 1 Department of Computer Science The Ohio State University anish@cis.ohio-state.edu Paul C. ATTIE 2 School of Computer Science Florida International University attie@fiu.edu E. Allen EMERSON 3 Department of Computer Sciences The University of Texas at Austin emerson@cs.utexas.edu 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 [EC82, MW84, PR89, PR89b, AM94]. 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, i.e., 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..