How can safety-critical systems be analyzed to ensure that dangerous states cannot occur?This video introduces the modeling and analysis of safety-critical systems using Petri nets, focusing on a railway crossing as a representative example. The video explains how a railway crossing can be modeled as a Petri net and how the corresponding reachability graph can be used to formally verify safety properties. In particular, it is shown that the model guarantees that the crossing gates cannot be open while a train has a green signal to pass the crossing. The example demonstrates how formal modeling and state-space analysis support reasoning about correctness and safety in systems where failures may lead to serious harm. The video illustrates how Petri nets provide a rigorous foundation for the design and validation of safety-critical control systems. Related resource:- WoPeD homepage and download: https://woped.dhbw-karlsruhe.de This is video #49 of the BPASeries.