Modular and Incremental Analysis of Concurrent Software Systems

11 years 10 months ago
Modular and Incremental Analysis of Concurrent Software Systems
Modularization and abstraction are the keys to practical verification and analysis of large and complex systems. We present in an incremental methodology for the automatic analysis and verification of concurrent software systems. Our methodology is based on the theory of abstract interpretation. We first propose a compositional data flow analysis algorithm that computes invariants of concurrent systems by composing invariants generated separately for each component. We present a novel compositional rule allowing us to obtain invariants of the whole system as conjunctions of local invariants of each component. We also show how the generated invariants are used to construct, almost , finite state abstractions of the original system that preserve safety properties. This reduces dramatically the computing such abstractions as reported in previous work. We finally give a novel refinement algorithm that refines the constructed abstraction until the property of interest is proved or a counte...
Hassen Saïdi
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where KBSE
Authors Hassen Saïdi
Comments (0)