Abstract
The synthetic system composite of cyber system and physical environment is hard to be modelled. It results that the formal verification for the interacted embedded software is very complicated. Integrated three kinds of timed automata, a systematic modelling approach is proposed in this paper for the embedded system with physical environment and artificial intermediary. All cyber-physical system components including embedded program, environment and their interface are formalized into timed automata. The behavior of real-time system is modeled as formal notation effectively. Based on visual modelling and auto verification tool the system simulation and specification verification have been achieved. A case study of path traversing for automated guided vehicle is given to illustrate our approach.