Đặc tả và kiểm chứng là các giai đoạn quan trọng, mang tính chất quyết định đối với chất lượng của hệ thống phần mềm. Bởi vậy, việc lựa chọn phương pháp, công cụ sử dụng trong đặc tả và kiểm chứng là một trong những vấn đề quan trọng cần phải xem xét. Trong bài báo này, chúng tôi trình bày phương pháp đặc tả hệ thống ATM bằng ngôn ngữ mô hình hóa Java (Java Modeling Language - JML) và tiến hành kiểm chứng tự động thông qua công cụ OpenJML tích hợp trên môi trường lập trình Eclipse. Phương pháp đặc tả và kiểm chứng thể hiện tính khả thi và tin cậy khi áp dụng vào tiến trình xây dựng cũng như phát triển các hệ thống phần mềm.
Specification and verification are essential phases, contributing to the quality of the software system. Therefore, the selection of methods and tools employed in these stages must be taken into account. In this paper, Java Modeling Language (JML) for specification ATM system and OpenJML(integrated to Eclipse environment) for automatic verification are thoroughly investigated. The result of the research has proven the feasibility and reliability of this technique in the researching and developing process of the software systems.