Safety analysis in Systems Engineering (SE) processes, as usually
implemented, rarely relies on formal methods such as model-checking
since such techniques, however powerful and mature, are deemed too
complex for an efficient use.
This paper thus aims to improve verification practice in SE design:
considering the widely used model of EFFBD (Enhanced Function Flow
Block Diagram), it formally establishes its syntax and behavioral
semantics. 
It also proposes a structural translation of EFFBDs to transition time
Petri Nets (TPNs); this translation is then proved to preserve the
behavioral semantics (i.e. timed bisimilarity). 
After proving results on the boundedness of the resulting TPNs, it was
possible to extend a number of fundamental properties (such as the
decidability of liveness, state-access etc.) from bounded TPNs to a
subclass of EFFBDs. 
Finally, these results led to the implement and integrate an
operational formal verification tool within a development platform
(used in systems design for defense applications) which underlying
complexity is totally concealed to the end-user.