Synchronous languages have been proposed to specify reactive Real-Time systems. Since such systems are used in safety critical areas, their formal verification is crucial. For machine and human efficiency, modular verification is advisable. For the synchronous language Argos, a Statechart variant, modular verification means having a method compatible with parallel composition and refinement. We present a translation of Argos programs into Boolean Automata. This translation enlightens the relation between refinement and parallel composition. We deduce modular verification results for properties expressed as VCTL~* formulas.
展开▼
