This technical report describes the EFFBD (Enhanced Function Flow
Block Diagram) formalism, widely used for the behavioral modeling and
analysis of complex engineering systems. The report formally
establishes the syntax and behavioral semantics of EFFBDs. It also
proposes a structural translation of EFFBDs to time Petri nets
(TPNs); this translation is then proved as preserving the behavioral
semantics through timed bisimilarity.

After proving results on the boundedness of the resulting TPNs, it
was possible to extend a number of fundamental properties (such as
liveness, state-access etc. decidability) from bounded TPNs to a
subclass of EFFBDs.