Translating SA/RT Models to Synchronous Reactive Systems: An Approximation to Modular Verification using the SMV Model Checker

Translating SA/RT Models to Synchronous Reactive Systems: An Approximation to Modular Verification using the SMV Model Checker
Claudio de la Riva, Javier Tuya, José R. de Diego
Perspectives of System Informatics. Dines Bjorner, Manfred Broy, Alexandre V. Zamulin (Eds.), Springer-Verlag, Vol. LNCS #1755, pp. 493-502, Febrero 2000

Abstract

Integration of non formal methods, notations and tools with formal ones is a promising way of linking scientific results to the daily work of practitioners. In this paper, we present a formal notation based in a synchronous reactive execution semantics (Synchronous Reactive System) for graphical specifications (SA/RT models). We use the Synchronous Reactive System as intermediate format to formally verify graphical specifications using the SMV model checker. We deal with the state space explosion problem using modular verification.

Index - Testing - Personal Page