SCSM - synchronous composition of sequential machines

Abstract

The SCSM formalism allows to define event driven synchronous systems by means of expressions formed by sum, product and restriction operators applied to non-deterministic sequential machines. Deterministic expressions are obtained through global product restrictions, which correlate transitions of non-deterministic components with states of other components. SCSM is usefull as denotation domain for synchronous system description languages, especially for models concerning reactive systems.