Translating SA/RT Models to Synchronous Reactive Systems: An Approximation to Modular Verification

Translating SA/RT Models to Synchronous Reactive Systems: An Approximation to Modular Verification
Claudio de la Riva, Javier Tuya, José R. de Diego
In: 3rd International Conference Perspectives of System Informatics, Akademgorodok, Rusia, pp. 378-384, 1999
Ext. Abstract (ps.zip)

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