Distributed systems are complicated real-time systems, which have been used in many safety-critical domains. In order to ensure the real-time constraints over the tasks running on these systems, the traditional schedulability analysis techniques, based on worst-case response time analysis, usually consider the worst case which could never occur in real world applications, and therefore the obtained results are pessimistic. The model checking technique based on automata theory could exhaustively search the whole system state space and return precise results. By using formal methods to analyze the schedulability of tasks on distributed systems, this paper presents the formal task model on distributed systems. It uses action automata and environment automata to model the task execution semantics and the external event arrival patterns respectively. It also translates the schedulability analysis to the reachability analysis of the locations in automata network, and proves the decidability of schedulability under certain scheduling policies with attached conditions and scope. Based on these conclusions, the formal check model implements a schedulability check tool, SCT (schedulability checking tool), and compares it with other techniques and tools on accurateness and performance. The comparisons show that SCT always provides the most accurate results but with the longest execution time.