文档介绍：AutomaticSynthesisofFault-puterScienceandEngineeringDepartmentMichiganStateUniversityAdvisor:,Question:Howdoweadddesiredfault-tolerancepropertiestop inordertocreateanewprogramp’suchthat:Requirements:Intheabsenceoff,theresultingfault-tolerantprogramp’behavessimilartopInthepresenceoff,theresultingfault-tolerantprogramp’satisfiesthedesiredfault-’’frompCorrectbyconstruction3PreviousWorkonAutomatedSynthesis4Synthesis: Specification-BasedSpecificationofp(TemporalLogicExpressions/Automata)SynthesisAlgorithm(provethesatisfiabilityofthespecification)FaultsFault-tolerancerequirements(TemporalLogicExpressions)Fault-tolerantprogramp’Programsynthesis: Fault-Tolerancesynthesis:[EmersonClarke1982] [AroraAttieEmerson1998][AttieEmerson2001][KupfermannVardi2001]5Synthesis: Calculational[KulkarniArora2000][KulkarniAroraChippada2001]Fault-intolerantprogramp(Transitions)SynthesisAlgorithm(Calculatethesetoftransitions)Fault-tolerantprogramp’(Transitions)Fault-tolerancerequirementsFaults(Transitions)plexityofCalculationalSynthesisHighatomicitymodel:processescanatomicallyread/writeallprogramvariablesPolynomialinthestatespaceofthefault-intolerantprogramp[KA00]Lowatomicitymodel(distributedprograms):processeshaveread/writerestrictionswithrespecttoprogramvariablesExponentialinthestatespaceofthefault-intolerantprogrampforsynthesizingmaskingfault-tolerance[KA00][KA00],Automatingtheadditionoffault-tolerance,-tolerantdistributedprograms7OutlinePreliminaryconceptsSynthesisproblemCurrentresultsTheoreticalissuesStep-wiseautomationPolynomial-timeboundaryHeuristicsPre-synthesizedfault-ponentsPracticalissuesAframeworkforthesynthesisoffault-tolerantprogramsContributionsOpenproblems8PreliminaryConcepts: ProgramsandFaultsProgr