Timed Models in AltaRica 3.0

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 thell probability of event occurrence. In this work, we explore the potentialities of AltaRica’s semantics and tools to express and analyze the timed properties of critical safety systems. To evaluate this approach, a case study involving two autonomous drones performing an obstacle avoidance maneuver is used. Our findings shed light on the strengths and limitations of using AltaRica for time-sensitive verification and provide insights into its applicability for real-world, time-critical safety assessments.