Modular design of reactive systems

We concentrate on two major aspects of reactive system design: behavior control and modularity. These are studied from a formal point of view, within the framework of action systems. The traditional interleaving paradigm is completed with a new barrier synchronization mechanism. This is achieved by introducing a new parallel composition operator, applicable to both discrete and hybrid models. While offering improvements with respect to control and modularity, the approach uses the correctness preserving mechanisms provided by the underlying reasoning environment.