Dynamic Analysis
of SA/RT Models using SPIN
Javier Tuya, José R. De Diego, Claudio de la Riva, José A. Corrales
In: 2nd International Workshop on the SPIN Verification System, New Brunswick,
New Jersey, pp. 36-50, 1996
(ps.zip)
Abstract
This paper presents the integrated use of the Spin Model Checker in conjunction
with Structured Methods (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. The above approach is then
illustrated using a steam boiler system as a case study.
Index - Testing
- Personal Page