This paper describes how verification practice in Systems Engineering
(SE) can be improved by providing efficient and usable tools based on
model-checking methods in order to perform 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. In particular, we
propose some decidability and complexity results for a temporal logic
adapted to EFFBDs enabling to express major, safety-critical properties
on high-level objects. As an application of these results, we developed
a simulation and verification software tool that benefits from TPNs
powerful analysis techniques (in particular by implementing efficient
algorithms) while concealing the inherent complexity to the end-user.