Autonomous Underwater Vehicles are increasingly used in missions for marine applications. However, the particular characteristics of underwater vehicles and their environment make testing the vehicles’ behavior in operational conditions extremely expensive. Yet, safety validation is an essential requirement for deploying underwater vehicles. Formal models for safety analysis can lower the cost of operational testing and validation for these systems, as they would allow detecting many problems earlier. Nevertheless, the literature still lacks the design of formal models which could serve as specifications in model-in-the-loop testing of the underwater controllers. This paper proposes modeling the underwater vehicle’s behavior as Timed Automata, and discusses examples of safety property patterns which can be handled by Timed Automata monitors and Timed CTL properties. The goal is to build a set of specifications (models and properties) which can then be used for testing and validation of controllers in underwater vehicles.