1Automated Revision of Existing ProgramsSoftware Engineering and Network Systems Laboratory (SENS)Borzoo BonakdarpourAutomated Revision of Existing Programs2MotivationQuestion : Is it possible to revise the model automatically such that it satisfies the failed property while preserving the other properties?CounterexampleCounterexampleModelPropertyModelCheckerAutomated Revision of Existing Programs3Motivation (cont’d)RequirementsQuestion : Is it possible to add a newly discovered property to an existing program automatically?SpecificationSpecificationDesignerProgramIncomplete Incomplete SpecificationSpecificationNew Property2Automated Revision of Existing Programs4Outline What is program revision? Adding properties to existing programs Results Example Adding fault-tolerance to existing real-time programs Results Example Ongoing research, Open problems, and Future workAutomated Revision of Existing Programs5Program Revision Revision by synthesis From specification: Comprehensive revision Highly expensive No reusability From the existing program + new property: Local revision Provides reusability In some cases, offers lower classes of time and space complexity Does not need to have the entire specification of the existing programRevisionAlgorithmProgram PProperty ΠP ′Π╨Automated Revision of Existing Programs6Our Goal We 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 complex?Why comprehensive revision is highly complex?AnswerAnswer::Expressiveness of specificationsExpressiveness of specifications3Automated Revision of Existing Programs7Part I:Adding PropertiesProperties to Existing ProgramsAutomated Revision of Existing Programs8Preliminary Concepts A 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 , …〉 iff s0∈ Ip ∀ i > 0 : (si-1 , si) ∈δp If σterminates in state sfthen there does not exist s such that (sf, s) ∈δp.Automated Revision of Existing Programs9Preliminary Concepts (cont.) Sample Properties Safety: P unless Q : stable(P): invariant(P): Liveness: P leads-to Q:P QP PP P P PPP PP P P Q4Automated Revision of Existing Programs10Preliminary Concepts (cont.) A specification is a conjunction of a set of properties:spec = L1∧ L2 ∧ … ∧ Ln A 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 Programs11Problem Statement Formulation of the problem: p′satisfies existing specification spece Sp′= Sp Ip′= Ipδp′⊆δp All computations of p′ are infinite satisfy specn.SynthesisAlgorithmProgram p = 〈Sp, Ip, δp〉Program p′= 〈Sp′, Ip′, δp′〉A Specification specnAutomated Revision of Existing Programs12Adding a Single Leads-to Property (R→ T )SpIpR TCase 1 : Deadlock statesRemove transitions (s1, s2) if s2∈ R and T is not reachable from S2s0s1s25Automated Revision of Existing Programs13Adding a Single Leads-to Property (R→ T )SpIpR TBreak cycles reachable from R without reaching Q.s1s4s2s3Case 2: Cycless0Automated Revision of Existing Programs14Soundness and Completeness Theorem (1) The algorithm for adding multiple safety properties along with a leads-to property is sound and complete. Fixability Theorem (2) The complexity of the algorithm for adding multiple safety properties along with a leads-to property is polynomial-time.Automated Revision of Existing Programs15Adding Two Leads-to Properties Adding two leads-to properties one after anotherSpIpRTs5s6s3s4s7PQs9s0s6s1s2s86Automated Revision of Existing Programs16Other Results The problems of simultaneous addition of two leads-toproperties is NP-complete. The problem of adding one leads-to property while maintaining maximum non-determinism is NP-complete.Automated Revision of Existing Programs17Another ProblemAdding two eventually properties1. true leads-to Q:2. true leads-to T:This problem is also NP-complete!QTAutomated Revision of Existing Programs18Example: Real-Time Resource Allocation Two 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 →≤ 2req.1){x}{x}7Automated Revision of Existing Programs19Automated Revision of Existing Programs20Example (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 Programs21Part II:Adding FaultFault--ToleranceTolerance to Existing Programs8Automated Revision of Existing Programs22The 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 Programs23The Byzantine Agreement ProblemThe Byzantine Agreement ProblemByzantine?b.g ∈ {false, true}b.jb.k ∈ {false, true}b.lByzantine?(b.j , b.k , b.l , b.g = false) → b.j := true(b.j := true) → d.j := 0|1Faults:Automated Revision of Existing Programs24The Byzantine Agreement ProblemThe Byzantine Agreement Problem Safety specification Agreement: The final decision of any two non-Byzantine process cannot be different. Validity: If the general is non-Byzantine then the final decision of a non-Byzantine process must be the same as that of the general. Fact : The program does not meet the safety specification in the presence of faults: d.g = 0, b.g = true d.j = 0, f.j = false → f.j := true d.k = 1, f.k = true9Automated Revision of Existing Programs25The Byzantine
View Full Document
Unlocking...