CSKH01.2019 - (Abstract) - This paper proposes a method for modeling and verifying UML 2.0 sequence diagrams using SPIN/PROMELA. The key idea of this method is to generate models that specify behaviors of each object in the given UML 2.0 sequence diagrams. In this paper, I/O automata are used as the models to maintain the interaction among objects. This work also proposes a mechanism to translate these models into PROMELA to use SPIN for checking the correctness of the system. By ensuring software design correctness, several properties can be guaranteed such as safety, stability, and the fact that no vulnerability is left. A support tool for this method is presented and tested with some particular systems to show the accuracy and effectiveness of the proposed method. This approach has promising potential to be applied in practice.