Report

VERIFICATION OF PARAMETERIZED SYSTEMS MONOTONIC ABSTRACTION IN PARAMETERIZED SYSTEMS Parosh Aziz Abdullah, Giorgio Delzanno, Ahmed Rezine NAVNEETA NAVEEN PATHAK AGENDA INTRODUCTION PARAMETERIZED TRANSITION SYSTEMS SYSTEMS ORDERING MONOTONIC ABSTRACTION Monotonic Abstraction in Parameterized Systems 2 INTRODUCTION Monotonic Abstraction as a simple and effective method to prove safety properties for Parameterized Systems with linear topologies. Main idea : Monotonic Abstraction for considering a transition relation that is an overapproximation of the one induced by the parameterized system. Monotonic Abstraction in Parameterized Systems 3 MODEL CHECKING + ABSTRACTION Infinite-State System Abstraction Model Checking Finite-State System Monotonic Abstraction in Parameterized Systems 4 AGENDA INTRODUCTION PARAMETERIZED TRANSITION SYSTEMS SYSTEMS ORDERING MONOTONIC ABSTRACTION Monotonic Abstraction in Parameterized Systems 5 PARAMETERIZED SYSTEMS P1 P2 P3 PN P4 P3 PN ......... P2 P1 .......... ......... AIM : To verify correctness of the systems for the whole family of Parameterized Systems. Monotonic Abstraction in Parameterized Systems 6 DEFINITION A parameterized system P is a triple (Q,X, T ), Q - set of local states, X - set of local variables, T - set of transition rules. A transition rule t is of the form: t: [ q | grd → stmt | q´ ] where q, q´ ϵ Q grd → stmt is a guarded command grd ϵ B(X) U G(X U Q) stmt : set of assignments Monotonic Abstraction in Parameterized Systems 7 Parameterized System, P = (Q,T) A process Q = {Green, Black, Blue, Red} and T = {t t t t t t } 1, 2, 3. 4, 5, 6 moves from where t t t – Local transition Idle State – Initially all rules 2, 5, 6 Idle to Black processes are in this t1, t4 – Universal Rules state when it state t3 – Existential Rule wants to access its critical section. Once a process moves from Black to Blue state, it “closes the door” on all processes in Idle state ∃L t3 V LR t1 t2 t6 t5 Critical State – Eventually a process will enter this state t4 VL Monotonic Abstraction in Parameterized Systems 8 AGENDA INTRODUCTION PARAMETERIZED TRANSITION SYSTEMS SYSTEMS ORDERING MONOTONIC ABSTRACTION Monotonic Abstraction in Parameterized Systems 9 TRANSITION SYSTEMS A transition system T is a pair (C,⇒) where, C - (infinite) set of configurations , ⇒ - binary relation on C, ⇒* - reflexive transitive closure of ⇒ A configuration c ϵ C is a sequence u1 , ...... , un of process states. i.e. corresponding to an instance of the system with n processes. Monotonic Abstraction in Parameterized Systems 10 The word below represents a configuration in an instance of system with 5 processes. Valid Transitions t3 Invalid Transitions t3 Monotonic Abstraction in Parameterized Systems 11 Initial Configuration Bad Configuration All configurations that have atleast 2 RED processes AIM : Init * Bad ? Monotonic Abstraction in Parameterized Systems 12 AGENDA INTRODUCTION PARAMETERIZED TRANSITION SYSTEMS SYSTEMS ORDERING MONOTONIC ABSTRACTION Monotonic Abstraction in Parameterized Systems 13 ORDERING c1, c2 – configurations c1 ≤ c2 - c1is a subword of c2 e.g. ≤ Upward Closed Configurations Set U of configurations is upward closed, if whenever c ϵ U and c ≤ c´ then c´ϵ U. c – configuration, ĉ – denotes upward closed set U:= {c´ | c ≤ c´} ĉ contains all configurations larger than c w.r.t. ordering ≤. i.e. c is the generator of U Monotonic Abstraction in Parameterized Systems 14 Why Upward Closed Sets ? 1. All sets of Bad configurations (which are worked upon) are upward closed. 2. Upward closed sets have an efficient symbolic representation. i.e. For an upward closed set U, there are configurations c1, ..... , cn with U = ĉ1 U......U ĉn Monotonic Abstraction in Parameterized Systems 15 Coverability Problem for Parameterized Systems To analyze safety properties. PAR-COV Instance • Parameterized System, P = (Q,X,T) •CF – upward-closed set of configurations Question * Init CF ? Monotonic Abstraction in Parameterized Systems 16 Backward Reachability Analysis For a set of configurations, C Use Pre(C) := {c | ∃c´ϵ C; c → c´} IDEA : i. Start with set of bad upward-closed configurations. ii. Apply function Pre repeatedly generating sequence U0, U1, U2,.... where U0 := Bad, and Ui+1 := Ui + Pre(Ui) for all i ≥ 0 Observation : set Ui characterizes set of configurations from which set Bad is reachable within i steps Monotonic Abstraction in Parameterized Systems 17 MONOTONICITY Monotonicity implies that upward closedness is preserved through the application of Pre. Consider: U – upward closed set, c1 – member of Pre(U) and c2 ≥ c1 By Monotonicity, it can be proved that c2 is also a member of Pre(U) Monotonic Abstraction in Parameterized Systems 18 AGENDA INTRODUCTION PARAMETERIZED TRANSITION SYSTEMS SYSTEMS ORDERING MONOTONIC ABSTRACTION Monotonic Abstraction in Parameterized Systems 19 MONOTONIC ABSTRACTION An abstraction that generates over-approximation of the transition systems. The abstract transition system is monotonic. Hence, allowing one to work with upward closed sets. c1 c1´ ≥ A c2 Monotonic Abstraction in Parameterized Systems 20 Local transitions are monotonic! Consider the local transition, t2 c1 = = c3 Configuration c2 = c2 = t2 c4 This leads to c4 ≥ c2 and also maintains c3 ≤ c4. Monotonic Abstraction in Parameterized Systems 21 Existential transitions are monotonic! Consider the existential transition: t3 c1 = = c3 Configuration, c2 = t3 c2 = = c4 Leading to c4 ≥ c3 Monotonic Abstraction in Parameterized Systems 22 Non-monotonicity of Universal transitions Consider the following Universal transition: c1 = t4 = c3 t4 can be applied to c1 as all process in the left context of the active process satisfy the condition of transition. Now consider c2 = c 1 ≤ c2 But t4 is not enabled from c2 since the left context of the active process violates the conditions of transition. Monotonic Abstraction in Parameterized Systems 23 Solution! 1. Work with Abstract transition relation →A. 2. →A is an monotonic abstraction (over-approximation) of the concrete relation →. 3. When t is universal, t t we have: c1 → c iff c ´ → c2 for some c1´ ≤ c1 A 2 1 t4 → i.e. A Since ≤ Monotonic Abstraction in Parameterized Systems t4 → 24 Solution..... Since, c1 ≤ c2 c1 →A c3 implies c2 →A c3 Hence, Abstract transition relation is Monotonic, w.r.t. Universal Transitions. The Abstract transition relation is and over-approximation of the original transition relation ↓↓ If a safety property holds in the abstract model, then it will also hold in the concrete model. Monotonic Abstraction in Parameterized Systems 25 Coverability Problem for Approximate Systems APRX-PAR-COV Instance • Parameterized System, P = (Q,X,T) •CF – upward-closed set of configurations Question * Init A CF ? Monotonic Abstraction in Parameterized Systems 26 A 1 =( U 1) reflects the approximation of universal quantifiers Since ⊆ A A negative answer to APRX-PAR-COV implies a negative answer to PAR-COV. Monotonic Abstraction in Parameterized Systems 27 CONCLUSION Monotonic Abstraction in Parameterized Systems 28 Introduction to our topic. Overview of Parameterized Systems using a simple example. (Infinite) Transition Systems arising from parameterized systems. Introduced Ordering on the set of configurations. Definiton and explanation of Monotomic Abstraction; based on the parameterized systems example. Monotonic Abstraction in Parameterized Systems 29 Thank you for your attention. Monotonic Abstraction in Parameterized Systems 30