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ỉ thiệt hại về mặt kinh tế mà còn có thể làm tổn thất trực tiếp sinh mạng con người. Do đó, nhu cầu nghiên cứu và đề xuất các phương pháp để kiểm chứng phần mềm ngày càng trở lên cần thiết. | Tóm tắt luận văn Thạc sĩ Công nghệ thông tin Kiểm chứng các thành phần Java tương tranh Chương 1 Mở đầu Bối cảnh 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ỉ thiệt hại về mặt kinh tế mà còn có thể làm tổn thất trực tiếp sinh mạng con người. Do đó nhu cầu nghiên cứu và đề xuất các phương pháp để kiểm chứng phần mềm ngày càng trở lên cần thiết. Một số nghiên cứu liên quan Kiểm chứng thiết kế Edmunds đề xuất ngôn ngữ đặc tả trung gian OCB Object-oriented Concurrent-B-OCB để nối liền giữa đặc tả bằng Event-B với sự cài đặt của các chương trình hướng đối tượng tương tranh. Đặc tả OCB sẽ được chuyển tự dộng sang mô hình của Event-B và mã chương trình Java. Các chương trình Java được chuyển đổi sẽ tuân thủ theo đặc tả OCB của nó. Ben Younes và các tác giả khác đề xuất các luật để chuyển đổi từ đặc tả bằng biểu đồ hoạt động Activity Diagram của UML sang đặc tả bằng Event-B. Đóng góp chính của nghiên cứu này là chuyển đổi từ một đặc tả trực quan sang hình thức và chứng minh tự động một mô hình thỏa mãn các thuộc tính của nó. Tuy nhiên việc chuyển đổi chưa được thực hiện tự động hoàn toàn hơn nữa nghiên cứu này mới đưa ra một ví dụ để minh họa khả năng chuyển đổi của nó. 1 Chương 1 Mở đầu 2 Ball đề xuất các mẫu thiết kế để đặc tả sự tương tác giữa các tác tử phần mềm các mẫu thiết kế sau đó được chuyển đổi sang đặc tả bằng Event-B. Tuy nhiên việc chuyển đổi từ mẫu thiết kế sang đặc tả bằng Event-B chưa được tự động. Giao thức tương tác tương tác được đặc tả lại với Event-B dựa vào mẫu thiết kế của nó. Kiểm chứng mã nguồn J-LO Java Logical Observer là một công cụ kiểm chứng sự tuân thủ của các chương trình Java so với các đặc tả của nó bằng logic thời gian tuyến tính linear temporal logic . J-LO mở rộng trình biên dịch AspectBench để đan các mã aspect được sinh ra vào chương .
