Analysis of Reactive SystemsAmir PnueliMondays, 5:00-6:50 PMCopies of presentations and Lecture Notes will beavailable athttp://www.cs.nyu.edu/courses/spring06/G22.3033-05/index.htmTextbooks:• Model Checking by E.C. Clarke, O. Grumberg, and D. Peled, MIT Press, 2000.• Temporal Verification of Reactive Systems: Safety by Z. Manna and A. Pnueli,Springer, 1995.Analysis of Reactive Systems, NYU, Spring, 2006Lecture 1: Modeling Systems A. PnueliCourse OutlineThe course will focus on formal verification of reactive systems. The course willbe dedictaed to methods for the verification of large systems. The main topics wewill consider are:• Systems and their Specification by LTL, CTL, and CTL∗. model checking offinite-state systems using BDD techniques over the TLV tool.• Deductive verification of infinite-state systems, using theorem provers such asPVS, and STeP.• Abstracion methods for combining deductive principles with algorithmicmethods.Course grades will be determined based on assignments and a term project.Analysis of Reactive Systems, NYU, Spring, 2006 1Lecture 1: Modeling Systems A. PnueliClassification of ProgramsThere are two classes of programs:Computational Programs: Run in order to produce a final result on termination.Can be modeled as a black box.x ySpecified in terms of Input/Output relations.Example:The program which computesy = 1 + 3 + · · · + (2x − 1)Can be specified by the requirementy = x2.Analysis of Reactive Systems, NYU, Spring, 2006 2Lecture 1: Modeling Systems A. PnueliReactive ProgramsPrograms whose role is to maintain an ongoing interaction with theirenvironments.Examples: Air traffic control system, Programs controlling mechanical devicessuch as a train, a plane, or ongoing processes such as a nuclear reactor.Can be viewed as a green cactus (?)Such programs must be specified and verified in terms of their behaviors.Analysis of Reactive Systems, NYU, Spring, 2006 3Lecture 1: Modeling Systems A. PnueliA Framework for Reactive Systems Verification• A computational model providing an abstract syntactic base for all reactivesystems. We use fair Discrete structures (FDS).• A Specification Language for specifying systems and their properties. We usetemporal logics: CTL∗, CTL, and LTL.• An Implementation Language for describing proposed implementations (bothsoftware and hardware). Use SPL, a simple programming language and theSMV input language for hardware systems description.• Verification Techniques for validating that an implementation satisfies aspecification. Practiced approaches:Algorithmic verification methods for exploratory verification of finite-statesystems: Enumerative and Symbolic variants.A deductive methodology based on theorem-proving methods. Canaccommodate infinite-state systems, but requires user interaction.Analysis of Reactive Systems, NYU, Spring, 2006 4Lecture 1: Modeling Systems A. PnueliFair Discrete SystemsA fair discrete system (FDS) D = hV, Θ, ρ, J , Ci consists of:• V – A finite set of typed state variables. A V -state s is an interpretation of V .ΣV– the set of all V -states.• Θ – An initial condition. A satisfiable assertion that characterizes the initialstates.• ρ – A transition relation. An assertion ρ(V, V′), referring to both unprimed(current) and primed (next) versions of the state variables. For example,x′= x + 1 corresponds to the assignment x := x + 1.• J = {J1, . . . , Jk} A set of justice (weak fairness) requirements. Ensure that acomputation has infinitely many Ji-states for each Ji, i = 1, . . . , k.• C = {hp1, q1i, . . . hpn, qni} A set of compassion (strong fairness) requirements.Infinitely many pi-states imply infinitely many qi-states.Analysis of Reactive Systems, NYU, Spring, 2006 5Lecture 1: Modeling Systems A. PnueliA Simple Programming Language: SPLA language allowing composition of parallel processes communicating byshared variables as well as message passing.Example: Program ANY-YConsider the programx, y : natural initially x = y = 0ℓ0: while x = 0 do[ℓ1: y := y + 1]ℓ2:m0: x := 1m1:− P1− − P2−Analysis of Reactive Systems, NYU, Spring, 2006 6Lecture 1: Modeling Systems A. PnueliThe Corresponding FDS• State Variables V :x, y : naturalπ1: {ℓ0, ℓ1, ℓ2}π2: {m0, m1}.• Initial condition:Θ : π1= ℓ0∧ π2= m0∧ x = y = 0.• Transition Relation: ρ: ρI∨ ρℓ0∨ ρℓ1∨ ρm0, with appropriate disjunct for eachstatement. For example, the disjuncts ρIand ρℓ0areρI: π′1= π1∧ π′2= π2∧ x′= x ∧ y′= yρℓ0: π1= ℓ0∧x = 0 ∧ π′1= ℓ1∨x 6= 0 ∧ π′1= ℓ2∧ π′2= π2∧ x′= x ∧ y′= y• Justice set: J : {¬at−ℓ0, ¬at−ℓ1, ¬at−m0}.• Compassion set: C: ∅.Analysis of Reactive Systems, NYU, Spring, 2006 7Lecture 1: Modeling Systems A. PnueliComputationsLet D be an FDS for which the above components have been identified. Thestate s′is defined to be a D-successor of state s ifhs, s′i |= ρD(V, V′).We define a computation of D to be an infinite sequence of statesσ : s0, s1, s2, ...,satisfying the following requirements:• Initiality: s0is initial, i.e., s0|= Θ.• Consecution: For each j = 0, 1, ..., the state sj+1is a D-successor of thestate sj.• Justice: For each J ∈ J , σ contains infinitely many J-positions• Compassion: For each hp, qi ∈ C, if σ contains infinitely many p-positions, itmust also contain infinitely many q-positions.Analysis of Reactive Systems, NYU, Spring, 2006 8Lecture 1: Modeling Systems A. PnueliExamples of ComputationsIdentification of the FDS DPcorresponding to a program P gives rise to a set ofcomputations Comp(P ) = Comp(DP).The following computation of program ANY-Y corresponds to the case that m0is the first executed statement:hπ1: ℓ0, π2: m0; x: 0 , y: 0im0−→ hπ1: ℓ0, π2: m1; x: 1 , y: 0iℓ0−→hπ1: ℓ2, π2: m1; x: 1 , y: 0iτI−→ · · ·τI−→ · · ·The following computation corresponds to the case that statement ℓ1isexecuted before m0.hπ1: ℓ0, π2: m0; x: 0 , y: 0iℓ0−→ hπ1: ℓ1, π2: m0; x: 0 , y: 0iℓ1−→hπ1: ℓ0, π2: m0; x: 0 , y: 1im0−→ hπ1: ℓ0, π2: m1; x: 1 , y: 1iℓ0−→hπ1: ℓ2, π2: m1; x: 1 , y: 1iτI−→ · · ·τI−→ · · ·In a similar way, we can construct for each n ≥ 0 a computation that executesthe body of statement ℓ0n times and then terminates in the final statehπ1: ℓ2, π2: m1; x: 1 , y: ni.Analysis of