JAIST Repository: Specification and Verification of Inter-Component Constraints in CTL

JAIST Repository

https://dspace.jaist.ac.jp/

Title Specification and Verification of Inter-Component Constraints in CTL

Author(s) Nguyen, Truong Thang; Katayama, Takuya Citation

Issue Date 2005-09-21 Type Presentation Text version publisher

URL http://hdl.handle.net/10119/8326 Rights

Description

1st VERITE : JAIST/TRUST-AIST/CVS joint workshop on VERIfication TEchnologyでの発表資料, 開催 ：2005年9月21日∼22日, 開催場所：金沢市文化ホール 3F

1

Specification and Verification of

Inter-Component Constraints in CTL

Nguyen Truong Thang

Takuya Katayama

Japan Advanced Institute of Science and Technology – JAIST

{thang, katayama}@jaist.ac.jp

Contents

„

Component-Based Software

„

Software Verification

„

A Formal Model of Components

„

Incremental Verification of Component Consistency

„

Component Specification and Verification

3

CB Software (1/4)

„

Component-based software:

structured from a set components

- Ideally, components are plug-and-play.

- Flexible for changes: handling new functional requirements or operating platforms.

- E.g.: mobile phones → camera-equipped mobile phones.

„

Many current software practice are

essentially component-based.

- Feature-oriented software.

- Each feature is treated as a large component which is formed from several member

components.

199x: components with talking features only

2004: offering varieties of features via extra

components: - Email/MMS - Photo-shooting - Contact-less IC - Web browsing - Document Viewer - GPS etc. evolving

Component-Based Software (2/4)

„

Components:

- Component-Off-The-Shelf (COTS): independent components in which computation paths rarely interleave each other (only a single exit state, no reentry state).

- Component refinement: interleave at some degree.

- This work: focusing on refinement (also applicable to COTS). Specifically, a

property initially holds in B. How to verify that subsequent refinements like E and E’ still preserve p in the composition component.

… … … … … …

5

Specification and Verification of CBS (3/4)

„

Current practice in component technology:

- Component plugging: only up to the level of syntactical matching.

- The issue: after being plugged, the components are inconsistent with each other.

Specification and Verification of CBS (4/4)

„

An important issue of component-based software paradigm:

- Specifically, what to formally specify component consistency and how to verify it in consistent and efficient manner?

„

Solution:

- Component specification: enforced with interface-mapping compatibilities and consistency constraints.

- Verification: via Open Incremental Model Checking (OIMC).

- OIMC: using assumption at reentry states, checking if the preservation constraints

are preserved at the interface between components. If so, the consistency among components is guaranteed. (explained later in Software Verification section)

7

Contents

„

Introduction

„

Software Verification

- Model Checking: CTL and Assumption Model Checking

- Incremental Model Checking

„

A Formal Model of Components

„

Incremental Verification of Component Consistency

„

Component Specification and Verification

Model Checking & CTL (1/4)

„

CTL* logic: constructed from two quantifiers:

- A (for all paths) and E (for some path); plus five temporal operators: X (next), F (eventually), G (always), U (until), R (release).

„

CTL: a true subset of CTL*.

- 10 basic normal CTL properties: AX f, EX f, AF f, EF f, AG f, EG f, A [f U g], E [f U g], A [f R g], E [f R g]; where f and g are CTL or atomic propositions.

A [f U g] f f f g g g g EG f f f f f f

9

Model Checking & CTL (2/4)

„

Definition: The

closure set

, cl(p), of p is the set of all sub-formulae

of p.

- p is an atomic proposition: cl(p) = {p} - p is among AX f, EX f, AG f, EG f, AF f, EG f: cl(p) = {p} ∪ cl(f) - p is among A [f U g], E [f U g], A [f R g], E [f R g]: cl(p) = {p} ∪ cl(f) ∪ cl(g) - p = ¬f: cl(p) = cl(f) - p = f ∧ g or p = f ∨ g: cl(p) = cl(f) ∪ cl(g)

„

In model checking, the characteristic is inside-out.

- To verify p in a model M, all sub-formulae closure set cl(p) of p are in general checked on the way.

Assumption Model Checking (3/4)

„

Idea [Laster98]: 2 sequential modules M1, M2.

- Possible to model check within M1 only if knowing the labels at the interface states between M1 and M2 by representing the whole M2 with those labels.

- A critical note on AMC: There should be no circle involving the interface nodes of M1 and M2. M1 A [f U g] f f M2 f g g g g

=

M1 A [f U g] f f g g A [f U g]

Assumption model checking is reliable only if the assumed labels at the interface states are proper.

11

Incremental Model Checking (4/4)

…

B

E

The assumption made at this state represents the computation tree in B After assumption model checking in E, if the

constraints at this state are preserved, there is no need to check further in B.

„

Incremental verification (or Open

Incremental Model Checking)

[Fisler01 etc]:

- An application of Assumption Model Checking. - Difference from AMC: ensuring the

preservation of constraints.

- Efficient: model checking each component separately.

- Open: handling even unanticipated future changes.

„

OIMC:

- Focusing on component refinement, but also applicable to COTS.

- Initially, a property under consideration holds in a base component.

- The property is guaranteed to hold in the system as long as other components preserve constraints at the interface of the base

Contents

„

Introduction

„

Software Verification

„

A Formal Model of Components

„

Incremental Verification of Component Consistency

„

Component Specification and Verification

13

A Formal Model of Components (1/2)

„

A component is formally represented by a state

transition model:

- A set of states: S

- A set of input events: Σ - An initial state: s₀

- A state transition function: R: S x PL(Σ) → S

- Labeling function at states: L – showing a set of atomic propositions to be true at a given state.

„

Typical case: a base component B is extended

with an extension component E.

- B = <S_B, Σ_B, s_0B, R_B, L_B> (see figure in next page) - E = <S_E, Σ_E, ⊥, R_E, L_E> (⊥ : no-care value)

- B and E are either composite or primitive components.

„

Associated with a component is an interface of

two state sets.

- B: <exit, reentry> - at which control is released from/returned to the base.

- E: <in, out> - states receiving/returning control respectively

e1 [g] e2

A Formal Model of Components (2/2)

„

Interfaces of B and E to be mapped accordingly.

- Defining the compatible conditions for which ex ↔ i, o ↔ re. - ex ↔ i if

∧

[L_B(ex)] ⇒

∧

[L_E(i)], where

∧

is the inter-junction. - o ↔ re if

∧

[L_E(o)] ⇒

∧

[L_B(re)].

„

The composition model C = <S

_C

, Σ

_C

, s

_0B

, R

_C

, L

_C

> is defined via

elements of B and E.

- E can overrides some part of B.

e1 [f] e2 e1 [g] e2 exit state in-state out-state reentry state E e1 B

15

Contents

„

Introduction

„

Software Verification

„

A Formal Model of Components

„

Incremental Verification of Component Consistency

- Component Consistency

- A Theorem on Component Consistency

- Incremental Verification

- Scalability of Incremental Verification

„

Component Specification and Verification

„

Conclusion

Component Consistency

(1/5)

B

E

i3/f i₁/f i₀/¬f i₁/f i0/¬f i2/f

„

Definition: a property p holds on a

model M = (S, Σ, s

₀

, R, L) if M, s

₀

|= p.

„

Component consistency definition:

- In terms of CTL properties.

- Initially, p holds on B = (S_B, Σ_B, s_0B, R_B, L_B), i.e. B, s_0B |= p.

- E does not violate p on B if within C, p still holds at s_0B in C, i.e. C, s_0B |= p.

„

In the example: p = AG EX f

- Initially: B, i₀ |= p

- After composition, C, i₀ |= p

- E does not violate p in B in this case.

E does not violate B w.r.t p i₁/f i₀/¬f i3/f i₂/f

17

A Theorem on Component Consistency (2/5)

„

Definition: Given a model M, the truth values of a state s with

respect to a closure set cl(p), V

_M

(s, cl(p)) are

- ∀φ ∈ cl(p): if M, s |= φ then φ ∈ V_M(s, cl(p)). - Otherwise, ¬φ ∈ V_M(s, cl(p)).

„

Conformance condition: B and E conform with each other (with

respect to cl(p)) at an exit state ex if V

_E

(ex, cl(p)) = V

_B

(ex, cl(p)).

„

Theorem: Given a property p holding in B, E does

not violate p in B if B and E conform with each

other (w.r.t cl(p)) at all exit states.

Incremental Verification of Components

(3/5)

During verifying p on B, the preservation constraints pc(s) =

V

_B

(s, cl(p)) at any interface state s are recorded.

The algorithm of OIMC: within E (the refinement) only

1.

For each reentry state re in B, seeding pc(re), i.e. V

_B

(re, cl(p)),

at the corresponding mapped out-state o in E.

2.

For each in-state i in E: run the CTL assumption model checking

procedure in E to check sub-formulae φ, ∀φ ∈ cl(p).

3.

Checking if V

_E

(i1,cl(p)), V

_E

(i2,cl(p)), … are matched with the

preservation constraints V

_B

(ex1,cl(p)), V

_B

(ex2,cl(p)), … at

respective mapped exit states ex1, ex2 … of B.

Note: - In case of COTS, there is no assumption since no reentry states.

- Assumption model checking is then replaced by standard model checking. - The constraints stay the same as above.

19

Incremental Verification of Components

(4/5)

… Base

re/V_B(re,cl(p)) ex1/V_B(ex1,cl(p))

ex2/V_B(ex2,cl(p))

V_B(re,cl(p))

… Extension 1

prop. values prop. values values(i1)

checking if B and E agree on the truth values at ex1, i.e.

values (i1) = V_B(ex1,cl(p))

… V_B(re,cl(p))

Extension 2

prop. values prop. values values(i2)

checking if B and E conform at ex2, i.e. values (i2) = VB(ex2,cl(p))

Scalability of Incremental Verification (5/5)

„

Considering subsequent component refinements.

„

Theorem: The method preserves its incremental

characteristic for any subsequent extensions as long as E

_i

conform with C

_(i-1)

at all exit states between them.

- The complexity only depends on the size of E_n (extending the base C_(n-1)).

C

₀

C

₀

C

₁

C

₁

C

_(n-1)

C

_(n-1)

C

_n

C

_n

E

₁

E

₁

…

E

₂

E

₂

E

_n

E

_n

21

Contents

„

Introduction

„

Software Verification

„

A Formal Model of Components

„

Incremental Verification of Component Consistency

„

Component Specification and Verification

- Component Specification

- Component Composition

- Incremental Verification of Components

Component Specification (1/4)

„

Component-based software:

- Problem: components are often inconsistent after composition.

- Consistency: several types ⇒ focusing on CTL property preservation.

- This work: enforcing component matching in terms of consistency semantic.

„

Current component technology (OMG CORBA, Sun Java and

JavaBeans, Microsoft .NET and COM/DCOM, UML/OCL etc):

semantic is limited to a simple logic of weak expressiveness and

syntactical component matching.

- Internal to components.

- Inter-component: Consumer.num_items ≤ Producer.num_items.

- The underlying logic only expresses constraints at the moment the interface element is invoked, i.e. static view.

„

Component specification:

- Interface signature: traditionally, attributes and operations (static and syntactical matching).

- Constraints: component matching in terms of semantic (via the interface compatibility in the formal model and the CTL consistency).

23

Component Composition (2/4)

„

Encapsulating temporal semantic constraints to component

interface via 2 constraint types.

- Plugging compatibility: for two components to be plugged together via exit-in and reentry-out states (p.11).

- Consistency constraint: making components to be consistent after being composed (p.15).

„

Consistency constraint:

- Written in CTL showing components’ execution traces, i.e. dynamic view. - Regarding to a CTL property p inherent to a component B, at an interface state s, its constraints are V_B(s, cl(p)).

„

Composing two components: C = B + E

- Signature (attributes and operations): the sum of those from B and E. - Plugging constraint: taken as L_B(s) or L_E(s) accordingly.

Incremental Verification of Components

(3/4)

V_B(s2, cl(p))

Constraints for future composition V_R(s1, cl(p))

V_R(s, cl(p)) = V_B(s, cl(p))

„

Initially, p holds in B.

„

B (Red) and E (Blue) are composed via

two exit states ex1, ex2 and a reentry

state re.

„

If V

_E

(ex1, cl(p)) = V

_B

(ex1, cl(p)) and

V

_E

(ex2, cl(p)) = V

_B

(ex2, cl(p)), E does

not violate p in B.

- only executed in E (i.e. incrementally).

…

re ex1

25

Incremental Verification of Components

(4/4)

…

Base Checking (Red)

re/V_B(re,cl(p)) ex1/V_B(ex1,cl(p))

ex2/V_B(ex2,cl(p))

V_B(re,cl(p))

…

Ext. Checking (Blue) 1

prop. values prop. values values(i1)

checking if B and E agree on the truth values at ex1, i.e.

values (i1) = V_B(ex1,cl(p))

… V_B(re,cl(p))

Ext. Checking (Blue) 2

prop. values prop. values values(i2)

checking if B and E conform at ex2, i.e. values (i2) = VB(ex2,cl(p))

Contents

„

Introduction

„

Software Verification

„

A Formal Model of Components

„

Consistency among Components

„

Component Specification and Verification

„

Conclusion

27

Conclusion (1/3)

„

Modular verification [Grumberg91, Kupferman98 etc]: based on

assume-guarantee paradigm

- Often dealing with hardware verification; modules are composed in parallel. - Verifying each module separately while assuming about the behaviors of the external environment and other modules.

- Interfaces are pre-defined and static.

- Verification task needs to re-run in the whole system if a new module is inserted or removed.

„

Modular software verification [Laster98]: exactly Assumption

Model Checking.

- Characteristically different from hardware verification. - Taking the advantage of sequential nature in software.

„

OIMC: the application of AMC in an open way (unanticipated future

evolution via component refinement).

Conclusion (2/3)

„

Open incremental model checking

- Interface is dynamically defined.

- Systems are more open for changes.

- Only model checking within the new module, i.e. incremental.

- The approach is also scalable for the whole evolution process as long as bases and extensions pair-wise conform.

„

Several research on software modules (components) compatibility

or consistency.

- Different types of consistency.

„

[Chakrabarti02]: interface compatibility among software modules

- Also state-based model.

- Focusing on different aspects of component semantic: correctness and completeness of operation definitions within components.

29

Conclusion (3/3)

„

OIMC is based on assumption model checking.

- AMC is not supported by well-known model checkers such as SMV, SPIN etc.

„

Improvement from current stage:

- Tool support: NuSMV2 is the target for adapting OIMC into real practice.

„

NuSMV2 is selected as the target because:

- open-source: comprehensibility and documentation.