Introducing automated formal methods for large industrial real-time systems is an important research challenge. We propose timed process automata for modeling and analysis of time-critical systems which can be open, ...