AN EFFICIENT REFINEMENT STRATEGY EXPLOITING COMPONENT PROPERTIES IN A CEGAR PROCESS

Embedded systems are usually composed of several com-ponents and in practice, these components generally have been independently verified to ensure that they respect their specifications before being integrated into a larger system. Therefore, we would like to exploit the specifica-tion (i.e. verified CTL properties) of the components in the objective of verifying a global property of the system. A complete concrete system may not be directly verifiable due to the state explosion problem, thus abstraction and eventually refinement process are required. In this pa-per, we propose a technique to select properties in order to generate a good abstraction and reduce refinement iterations. We have conducted several preliminary exper-imentations which show that our approach is promising in comparison to other abstraction-refinement techniques implemented in VIS [1]. Index Terms — Compositional verification, CTL properties, CEGAR, model-checkin