Marius Bozga, Vassiliki Sfyrla, Joseph Sifakis
Modeling Synchronous Systems in BIP (2009)
Modeling Synchronous Systems in BIP (2009)
TR-2009-8.pdf
Keywords: synchronous systems, priority Petri nets, modal flow graphs, BIP(Behavior-Interaction-Priority)
Abstract: We present a general approach for modeling synchronous component-based systems. These are systems of synchronous components strongly synchronized by a common action that initiates steps of each component. We propose a general model for synchronous systems. Steps are described by acyclic Petri nets equipped with data and priorities. Petri nets are used to model concurrent flow of computation. Priorities are instrumental for enforcing run-to-completion in the execution of a step. We study a class of well-triggered synchronous systems which are by construction deadlock-free and their computation within a step is confluent. For this class, the behavior of components is modeled by modal flow graphs. These are acyclic graphs representing three different types of dependency between two events $p$ and $q$: strong dependency (p must follow q), weak dependency (p may follow q), conditional dependency (if both p and q occur then p must follow q). We propose a translation of Lustre into well-triggered synchronous systems. This translation is modular and exhibits not only data-flow connections between nodes but also their synchronization by using clocks.
