Cài đặt (chương trình) thường không tự sinh ra từ đặc tả nên nó có thể vẫn có lỗi mặc dù thiết kế của nó đã được kiểm chứng là đúng. Để giải quyết các vấn đề này, tác giả đã đề xuất một phương pháp kiểm chứng sự tuân thủ của cài đặt so với đặc tả vào thời điểm thực thi. Phương pháp này có thể kiểm chứng được sự nhất quán giữa chương trình Java và đặc tả giao thức tương tác của nó, các vi phạm được phát hiện trong bước kiểm thử. | Kiểm chứng sự tương tác giữa các thành phần trong chương trình đa luồng sử dụng lập trình hướng khía cạnh Checking Interaction Protocol in Multi-threaded Program using AOP Trịnh Thanh Bình, Trương Anh Hoàng, Nguyễn Việt Hà Abstract: Interaction protocol specifies allowed method call sequences among classes or objects in a program. We propose an approach to verify interaction protocol for multi-thread programs. Our approach processes interaction protocol specified by extended regular expressions or protocol state machines in UML and generates aspect code to weave with the programs for runtime verification. The aspect code will monitor the execution of the program and check the conformance between the programs and their specifications. We implemented the approach as a tool for generating aspect code in AspectJ and checking Java programs. The experimental results show that our approach is convenient to use in practice. I. GIỚI THIỆU Phần mềm ngày càng đóng vai trò quan trọng trong xã hội hiện đại. Tỷ trọng giá trị phần mềm trong các hệ thống ngày càng lớn. Tuy nhiên, trong nhiều hệ thống, lỗi của phần mềm gây ra các hậu quả đặc biệt nghiêm trọng, không chỉ về mặt kinh tế mà còn về con người [16], đặc biệt là các phần mềm điều khiển hệ thống và thiết bị giao thông. Các phương pháp kiểm chứng hình thức như chứng minh định lý [8] và kiểm chứng mô hình [6, 7] đã đạt được thành công nhất định trong kiểm chứng đặc tả phần mềm. Cài đặt mã chương trình thường chỉ được thực hiện sau khi các đặc tả này đã được kiểm chứng. Tuy nhiên, cài đặt (chương trình) thường không tự sinh ra từ đặc tả nên nó có thể vẫn có lỗi mặc dù thiết kế của nó đã được kiểm chứng là đúng [16]. Để giải quyết các vấn đề này, chúng tôi đã đề xuất một phương pháp kiểm chứng sự tuân thủ của cài đặt so với đặc tả vào thời điểm thực thi [1,10]. Phương pháp này có thể kiểm chứng được sự nhất quán giữa chương trình Java và đặc tả giao thức tương tác của nó, các vi phạm được phát hiện trong bước kiểm .
