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 EFFBDs (Enhanced Function Flow Block Diagrams), it proposes a method
for a translation into Time Petri Nets (TPNs); known results are then
applied from TPNs to EFFBDs, leading to the possibility of assessing a
number of safety-critical properties. This paper also presents some
tools developed in application of these results and which the
underlying complexity is totally concealed from the end-user.