A component-based approach to verification and validation of formal software models.

摘要

Formal methods for verification of software systems often face the problem of state explosion and complexity. We present a divide and conquer methodology that leads to component based verification and analysis of formal requirements specifications expressed using Software Cost Reduction (SCR) models. The proposed methodology has the following steps: model partitioning, partition verification (either by model checking or testing) and composition of verification results.;We define a novel decomposition methodology for SCR specifications based on min-cut graph algorithms. The methodology identifies components in given SCR specifications and automates related abstraction methods. It also provides guidance on how to perform verification and validation of the formal system models. Further, we present a strategy for verification of modular and decomposable software models. Efficient verification of SCR models is achieved with the use of invariants and proof compositions.;SCR specifications can be executed by the simulator and tested, either automatically (e.g. random testing) or manually, guided by a domain expert using visual interface mimicking the actual system. Some of the identified specification components might be simple enough to allow thorough testing, despite having large state spaces that cause problems with model checking approaches. We define model test coverage measures and develop tools to track the achieved coverage during manual and random testing. Testing and coverage measures provide degree of assurance in the component correctness. Our experimental results also provide insight into the efficacy of random testing approaches for verification of software models.;Experimental validation of our methodology brought to light several concepts that have been advocated in the software development community for a long time: modularity, encapsulation, information hiding and the avoidance of global variables. The advantages of the compositional verification strategy are demonstrated in the case study, which analyses the Personnel Access Control System. Our approach offers significant savings in terms of time and memory requirements needed to perform formal system verification.