Naslov
A Component-Based Approach to Verification and Validation of Formal Software Models

Autori
Desovski, Dejan ; Cukic, Bojan

Vrsta, podvrsta i kategorija rada
Poglavlja u knjigama, ostalo

Knjiga
Architecting Dependable Systems IV

Urednik/ci
Lemos, R. de ; et. al.

Izdavač
Springer

Grad
Berlin

Godina
2007

Raspon stranica
89-114

ISBN
978-3-540-74033-9

Ključne riječi
ne
(none)

Sažetak
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 analysis and verification of formal requirements specifications expressed using Software Cost Reduction (SCR) models. The proposed methodology has the following steps: model partitioning, partition verification and composition of verification results. We define a novel decomposition methodology for SCR specifications based on minimum cut graph algorithms. Experimental validation of our methodology brought to light the importance of 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.

Izvorni jezik
Engleski

Znanstvena područja
Računarstvo

POVEZANOST RADA