Abstract: The soundness of the model is the key issue to guarantee the reliability of distributed real-time embedded （DRE） software. Reasonable determination method of DRE software model is given in this paper. The method is based on time Petri nets with inhibitor

Key words: Distributed real-time embedded software, Petri nets, Model, Soundness, Verification