CASE Support for Modular Verification of Synchronous Reactive Systems
Javier Tuya, Claudio de la Riva, Josť R. de Diego, Josť A. Corrales
In: 2nd International Workshop on Formal Methods for Industrial Critical Systems, Cesena, Italy, pp. 125-137, 1997


The execution of synchronous reactive systems like Esterel or some versions of Statecharts may be viewed as a sequence of instantaneous reactions to the inputs (macro-steps), where each macro-step is composed of a sequence of internal interactions (micro-steps). The usual approach to verification of such systems is to construct a global state transition graph and perform model checking on it. This paper presents a different approach: we build a model in which micro-steps are observable, and perform verification on it. We automate the translation from a graphical specification to the target language to be used for model checking: PROMELA/SPIN and SMV are currently supported. Also, since internal steps can be observed, we perform modular verification of safety properties using assumption/commitment rules, and show how the properties and the structure of the operational model are integrated into a declarative model using Property Diagrams.

Index - Testing - Personal Page