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
(ps.zip)
Abstract
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