A Strategy for Verification of Decomposable SCR Models

摘要

Formal methods for verification of software systems often face the problem of state explosion and complexity. We propose a divide and conquer methodology which leads to component-based verification and analysis of formal requirements specifications expressed using Software Cost Reduction (SCR) models. This paper presents a novel decomposition methodology which identifies components in the given SCR specification and automates related abstraction methods. Further, we propose a verification strategy for modular and decomposable software models. Efficient verification of SCR models is achieved through the use of invariants and proof compositions. Experimental validation of our methodology brought to light the importance of modularity, encapsulation, information hiding and the avoidance of global variables in the context of formal specification models. The advantages of the compositional verification strategy are demonstrated in the analysis of the Personnel Access Control System. Our approach offers significant savings in terms of time and memory requirements needed to perform formal system verification.