Embedded systems have become increasingly connected and communicate with each other, forming large-scaled and complicated network systems. To make their design and testing more reliable and robust, this paper proposes a formal specification language called SENS and a SENS-based automatic test generation tool called TGSENS. The authors' approach is summarized as follows: a user describes requirements of target embedded network systems by logical property-based constraints using SENS. Given SENS specifications, test cases are automatically generated using a SAT-based solver. Filtering mechanisms to select efficient test cases are also available in their tool. In addition, given a testing goal by the user, test sequences are automatically extracted from exhaustive test cases.