Temporal Verification of Real-Time Multitasking Application Properties Based on Communicating Timed Automata