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...

• Type: Conference
• Year: 1999
• Where: KBSE
• Authors: Hassen Saïdi
• Keywords: Abstract Interpretation, Generated Invariants, KBSE 1999, Local Invariants, Software Engineering