Automated Revision of Existing ProgramsMotivationMotivation (cont’d)OutlineProgram RevisionOur GoalSlide 7Preliminary ConceptsPreliminary Concepts (cont.)Slide 10Problem StatementAdding a Single Leads-to Property (R T )Slide 13Soundness and CompletenessAdding Two Leads-to PropertiesOther ResultsAnother ProblemExample: Real-Time Resource AllocationSlide 19Example (cont’d)Slide 21The Byzantine Agreement ProblemSlide 23Slide 24Slide 25Some TerminalogyPreliminaries (cont’d)Levels of Fault-Tolerance [3]Fault-Tolerant Real-Time ProgramsNew Levels of Fault-Tolerance for RT ProgramsLevels of Fault-Tolerance (cont’d)Slide 32Slide 33Current ResultsExample: Altitude SwitchOngoing ResearchConclusionSlide 39Automated Revision of Existing ProgramsSoftware Engineering and Network Systems Laboratory (SENS)Borzoo BonakdarpourAutomated Revision of Existing Programs 2MotivationQuestion : Is it possible to revise the model automatically such that it satisfies the failed property while preserving the other properties?CounterexampleCounterexampleModel PropertyModelCheckerAutomated Revision of Existing Programs 3Motivation (cont’d)RequirementsQuestion : Is it possible to add a newly discovered property to an existing program automatically?SpecificationSpecificationDesignerProgramIncomplete Incomplete SpecificationSpecificationNew PropertyAutomated Revision of Existing Programs 4OutlineWhat is program revision?Adding properties to existing programsResultsExampleAdding fault-tolerance to existing real-time programsResultsExampleOngoing research, Open problems, and Future workAutomated Revision of Existing Programs 5Program RevisionRevision by synthesisFrom specification: Comprehensive revisionHighly expensive No reusabilityFrom the existing program + new property: Local revisionProvides reusabilityIn some cases, offers lower classes of time and space complexityDoes not need to have the entire specification of the existing programRevisionAlgorithmProgram PProperty P ╨Automated Revision of Existing Programs 6Our GoalWe identify classes of interesting properties typically used in specifying reactive systems.Designing synthesis methods where revising existing programs is feasible time-wise and space-wise.QuestionQuestion :: Why comprehensive revision is highly Why comprehensive revision is highly complex?complex?AnswerAnswer :: Expressiveness of specifications Expressiveness of specificationsAutomated Revision of Existing Programs 7Part I:Adding PropertiesProperties to Existing ProgramsAutomated Revision of Existing Programs 8Preliminary ConceptsA program p is a triple p = Sp , Ip , p, i.e., finite state space, set of initial states, and program transitions.A state predicate is any subset of Sp.A computation is a state sequence s0 , s1 , … iffs0 Ip i > 0 : (si-1 , si) pIf terminates in state sf then there does not exist s such that (sf , s) p.Automated Revision of Existing Programs 9Preliminary Concepts (cont.)Sample PropertiesSafety:P unless Q :stable(P):invariant(P):Liveness:P leads-to Q:P QP PP P P PPP PP P P QAutomated Revision of Existing Programs 10Preliminary Concepts (cont.)A specification is a conjunction of a set of properties:spec = L1 L2 … LnA computation satisfies spec iff (i | 0 i n : satisfies Li)A program p satisfies spec iff all computations of p1. are infinite2. satisfy spec.Automated Revision of Existing Programs 11Problem StatementFormulation of the problem:p satisfies existing specification speceSp = SpIp = Ipp p All computations of pare infinitesatisfy specn.SynthesisAlgorithmProgram p = Sp , Ip , pProgram p = Sp , Ip , pA Specification specnAutomated Revision of Existing Programs 12Adding a Single Leads-to Property (R T )SpIpR TCase 1 : Deadlock statesRemove transitions (s1, s2) if s2 R and T is not reachable from S2s0s1s2Automated Revision of Existing Programs 13Adding a Single Leads-to Property (R T )SpIpR TBreak cycles reachable from R without reaching Q.s1s4s2s3Case 2: Cycless0Automated Revision of Existing Programs 14Soundness and CompletenessTheorem (1) The algorithm for adding multiple safety properties along with a leads-to property is sound and complete. FixabilityTheorem (2) The complexity of the algorithm for adding multiple safety properties along with a leads-to property is polynomial-time.Automated Revision of Existing Programs 15Adding Two Leads-to PropertiesAdding two leads-to properties one after anotherSpIpRTs5s6s3s4s7PQs9s0s6s1s2s8Automated Revision of Existing Programs 16Other ResultsThe problems of simultaneous addition of two leads-to properties is NP-complete.The problem of adding one leads-to property while maintaining maximum non-determinism is NP-complete.Automated Revision of Existing Programs 17Another ProblemAdding two eventually properties1. true leads-to Q:2. true leads-to T:This problem is also NP-complete!QTAutomated Revision of Existing Programs 18Example: Real-Time Resource AllocationTwo processes j {1, 2}.Each has two tasks to complete (each takes 1 time unit)Submitting a request Performing I/O operationRQj : req.j (x = 1) io.j, req.j := true, false ;IOj : io.j (x = 1) req.j, io.j := true, false ;WT : 0 x 1 � wait;Bounded response:L (io.1 2 req.1) {x} {x}Automated Revision of Existing Programs 19Automated Revision of Existing Programs 20Example (cont’d)RQ1 : req.1 (x = 1) io.1, req.1 := true, false ;IO1 : io.1 (x = 1) req.1, io.1 := true, false ;RQ2 : req.2 (x = 1) (io.1 t 1) io.2, req.2 := true, false ;IO1 : io.2 (x = 1) (io.1 t 1) req.2, io.2 := true, false ;WT : 0 x 1 � wait;{x, t} {x} {x} {x}Automated Revision of Existing Programs 21Part II:Adding Fault-ToleranceFault-Tolerance to Existing ProgramsAutomated Revision of Existing Programs 22The Byzantine Agreement ProblemThe Byzantine Agreement ProblemDecision d.g {0, 1}(d.j = ) ( f.j = false) d.j := d.g(d.j ) ( f.j = false) f.j := trued.jd.k {0, 1, } d.lDecisionf.jf.k {false, true} f.lFinal?GENERALNON-GENERALSProgram:Automated Revision of Existing Programs 23The
View Full Document
Unlocking...