Dynamic Analysis of SA/RT Models using SPIN and Modular Verification

Dynamic Analysis of SA/RT Models using SPIN and Modular Verification
Javier Tuya, José R. De Diego, Claudio de la Riva, José A. Corrales
The Spin Verification System. J-C Grégoire,G.J. Holzmann, D.A. Peled, Eds., American Mathematical Society, Vol. DIMACS/32, pp. 165-183, 1997

Abstract

We present a practical approach to use the SPIN model checker in conjunction with Structured Analysis methods for Real Time systems (SA/RT). The graphical model is translated into a PROMELA program in which we prove assertions about the desired behaviour of the system. We also provide support for modular verification, by separately verifying different components of the model and deducing the desired global properties from the previous verifications. This approach is then illustrated using a steam boiler system as a case study.

Index - Testing - Personal Page