Model-Based Safety Assessment is a cornerstone of modern safety-critical system design, providing formal verification techniques to ensure compliance with stringent safety requirements. The AltaRica 3.0 modeling language offers a structured approach to model system behavior and failures. The associated tools support qualitative and probabilistic risk analysis. In addition, the language semantics and the simulator integrate timing constraints associated with the probability of event occurrence. An exploration over the potentialities of AltaRica’s semantics and tools is presented: static, dynamic and timed properties of critical safety systems are expressed and analysed. To evaluate this approach, a case study involving two autonomous drones performing an obstacle avoidance manoeuvre is used. The findings shed light on the advanced ways of using AltaRica’s state machine formalism for time-sensitive verification and provide insights into its applicability for real-world, time-critical safety assessments.