A method is described for the analysis and the verification of safety in software systems. The method offers a formal notation for describing the software structure, the means for defining safe and unsafe states of the system and a technique for the software simulation and analysis. The modeling process is based on an extension to Petri nets, which enables the modeler to represent control as well as data processing aspects of the software. The Petri net-based model can be analyzed using the concept of a modified reachability tree or can be used as a framework for a simulated execution. The model can be build in an early phase of the software development process, thus creating the potential for early verification and validation of safety.