Compositional Abstraction Refinement for Component-Based Systems | Zendy

Lianyi Zhang | Zendy; Qingdi Meng | Zendy; Kueiming Lo | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Compositional Abstraction Refinement for Component-Based Systems

Author(s) -

Lianyi Zhang,

Qingdi Meng,

Kueiming Lo

Publication year - 2014

Publication title -

journal of applied mathematics

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.307

H-Index - 43

eISSN - 1687-0042

pISSN - 1110-757X

DOI - 10.1155/2014/703098

Subject(s) - counterexample , abstraction , computer science , component (thermodynamics) , invariant (physics) , theoretical computer science , model checking , formal verification , predicate abstraction , abstraction model checking , programming language , algorithm , mathematics , discrete mathematics , thermodynamics , philosophy , physics , epistemology , mathematical physics

The efficiency of the compositional verification ofinvariants depends on the abstraction, which may lead to verificationincompleteness. The invariant strengthening and statepartitioning techniques are proposed in this paper. The formercould refine the overapproximation by removing the unreachablestates, and the latter is a variant of counterexample-guidedabstraction refinement. Integrated with these two refinementtechniques, a unified compositional verification framework is presentedto strengthen the abstraction and find counterexamples. Some examples are included to show that the verification of thesafety properties in component-based systems has been achievedby our framework

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research