Phương pháp hình thức kiểm chứng hệ thống ATM sử dụng JML

  • Đào Thị Hường
Từ khóa: ATM, Đặc tả phần mềm, JML, kiểm chứng phần mềm

Tóm tắt

Đặ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.

điểm /   đánh giá
Phát hành ngày
2020-08-05