TinyOS applications for Wireless Sensor Networks (WSNs) typically run in a complicated concurrency model. It is difficult for developers to precisely predict the dynamic execution process of a TinyOS application by its static source codes. Such a conceptual gap frequently incurs software bugs, due to unexpected system behaviors caused by unknown execution patterns. This paper presents T-Morph (TinyOS application tomography), a novel tool to mine, visualize, and verify the execution patterns of TinyOS applications. T-Morph abstracts the dynamic execution process of a TinyOS application into simple, structured application behavior models, which well reflect how the static source codes are executed. Furthermore, T-Morph visualizes them in a user-friendly manner. Therefore, WSN developers can readily see if their source codes run as intended by simply verifying the correctness of the models. Finally, the verified models allow T-Morph to automatically check the application behaviors during a long-term testing execution. The suggested model violations can unveil potential bugs and direct developers to suspicious locations in the source codes. We have implemented T-Morph and applied it to verify a series of representative real-life TinyOS applications and find several bugs, including a new bug in the latest release of TinyOS. It shows T-Morph can provide substantial help to verify TinyOS applications.