Formal model and verification techniques can be used to design and analyze many kinds of systems. However, there are few formal models for verification and analysis of sensor networks in the literature. In this paper, we present a graphical simulation system for modeling and analysis of sensor networks. A formal model of sensor networks is proposed based on Space Time Petri Net (STPN). STPN is a formal model language which is extended from Time Petri Nets (TPN) and Colored Petri Nets (CPN). The idea is to add space information to the places of the original TPN to model the space information in sensor networks, such as the locations of sensor nodes. And based on this modeling idea, a set of new concepts are proposed, such as space place, broadcast transition, and dynamic topology. The STPN not only can model the various characteristics of sensor networks, such as temporal and spatial information, but also can simulate the different behavior of sensor networks. A prototype system has been implemented to model and analyze the behavior of sensor networks systems.