This paper describes how verification practice in Systems Engineering
can be improved by providing efficient and usable tools based on model
checking methods in safety and dependability analysis of complex, high
level models. We consider the widely-used model of Enhanced Functional
Flow Block Diagrams (EFFBDs); after proposing a structural translation
of EFFBDs to time Petri nets (TPNs), proved to preserve temporal
behavior, we were able to extend a number of fundamental theoretical
results on TPNs to EFFBDs. As an application of these results, we
developed a simulation and verification software tool that benefits
from TPNs powerful analysis techniques while concealing the inherent
complexity to the end-user.