dvi and
postscript
The example is originally due to Peleska, who argues that to achieve the combined service, it is necessary to strengthen one of the individual services to address both concerns. In contrast, I argue that the individual services should be "deconstructed" into smaller and weaker components that can be reassembled in different ways, and I show that the combined service can be achieved by composing the fault-tolerant service with a weaker version of the secure service.
The report also provides an introduction to the use of mechanized formal state exploration methods (specifically, the Murphi system from Stanford) for the purpose of examining and debugging protocols.
dvi and
postscript
@techreport{Rushby95:caution,
AUTHOR = {John Rushby},
TITLE = {Combining System Properties:
A Cautionary Example and Formal Examination},
INSTITUTION = {Computer Science Laboratory, SRI International},
MONTH = jun,
YEAR = 1995,
ADDRESS = {Menlo Park, CA},
NOTE = {Unpublished project report; available at \url{http://www.csl.sri.com/~rushby/combined.html}}
}
Return to the Formal Methods Program home page