Abstract: If the functional design of the Wireless Sensor Networks system ignores the interaction behaviors among the WSNs and the monitored entities,it will lead to the situation that a WSNs system itself is reliable but its monitoring en- tity’s safety is not warranted. This situation is very dangerous in industrial production process. In order to verify the re- liability and applicability of the functional design of WSNs monitoring system,the model of WSNs system was estab- lished based on time automaton model to check WSNs reliability. According to the relationship between sensors and mine environmental entities,the authors analyzed the parallel behaviors among the sensors and monitored entities in mine. Then,the authors proposed the timed automata model of the WSNs behaviors interacting with these entities,and established the description method of the applicability properties of the whole system. Based on the model,from the point of view of WSNs’ functional design,combining these interactive entities,the WSNs’ ability of monitoring pro- duction processes was tested to ensure the applicability of the system functions. Because some physical entities contain concurrent structures,the branch behavior equivalence was used to construct the concurrent time automaton models of entities. Moreover,using the method of mutual simulation of the concurrent branch aggregation behavior between enti- ties,the models of entities parallel behaviors were aggregated into one. The correctness of these methods was proved based on the equivalent mutual simulation. Thus,the number of the model states was reduced and the efficiency of the verification process was increased. Finally,aiming to the actual roadway deployment plan of the gas sensor in the cur- rent standards,the method to test gas sensor deployment solutions written in a current standard was used. Considering the entity’s concurrent behaviors,it was found that one of the gas sensor deployment solutions containing branch road- way with a potential missed detection of gas-leak. This checking method combining entities model needs an automatic establishment mechanism to improve its practicability.