ĐẶT VẤN ĐỀ 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. Nhưng 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, đặc biệt là các phần mềm điều khiển hệ thống và thiết bị giao thông. Nguyên nhân của các lỗi này là do phần mềm ngày càng phức tạp do các bài toán được giải quyết và hỗ trợ bởi phần mềm ngày càng lớn.
Để khắc phục các khó khăn này, cách tiếp cận hướng đối tượng đã được sử dụng để phát triển phần mềm và tỏ ra hiệu quả từ những năm 90 của thế kỷ trước[17]. Tuy nhiên, do độ phức tạp của phần mềm ngày càng cao và để giảm giá thành, kiến trúc phần mềm cần được cải tiến để tăng tính dùng lại (reuse) của các yếu tố phần mềm đã phát triển trước đó. Cách tiếp cận hướng thành phần được áp dụng rộng rãi và có hiệu quả cao. Theo cách tiếp cận này, phần mềm được xây dựng bằng cách lắp ráp các thành phần riêng biệt lại với nhau như được định nghĩa là: “Các thiết kế phần mềm mới được tạo ra bằng cách kết hợp các đơn thể phần mềm có sẵn với một phần mềm mới cung cấp các chức năng mới và mã kết nối các thành phần với nhau”.
Trong đó, thành phần phần mềm được định nghĩa bởi Szyperski năm 1997 là: “Thành phần phần mềm là một đơn vị của việc kết hợp với các giao diện được đặc tả bởi hợp đồng và có các mối phụ thuộc tường minh, có thể được triển khai độc lập và hướng tới việc kết hợp bởi bên thứ ba” [ 11]. Trong định nghĩa này, giao diện của thành phần được đặc tả bởi hợp đồng đóng vai trò mấu chốt. Hợp đồng bao gồm các dịch vụ và chất lượng dịch vụ mà thành phần phần mềm cung cấp cho môi trường và những điều kiện mà môi trường phải thỏa mãn để được nhận dịch vụ của thành phần. Câu hỏi đặt ra là làm thế nào để kiểm chứng xem môi trường (chương trình gọi đến các dịch vụ của phần mềm) có tuân thủ các điều kiện được mô tả trong hợp đồng của giao diện thành phần hay không.
Các phương pháp kiểm chứng hình thức như chứng minh định lý và kiểm chứng mô hình đã đạt được những thành công nhất định trong kiểm chứng và đặc tả phần mềm. Việc sử dụng các phương pháp này vào bài toán nêu trên hy vọng có nhiều hứa hẹn. Các điều kiện mô tả trong giao diện của thành phần gồm có các tiền điều kiện đối với các tham số của dịch vụ và thứ tự của các lời gọi dịch vụ mà môi trường phải tuân thủ (tức là giao thức). Tôi tập trung vào việc kiểm chứng điều LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 7 kiện thứ hai, tức là kiểm chứng xem môi trường có tuân thủ các thứ tự lời gọi được qui định hay không và tin rằng lời giải có thể được mở rộng để kiểm tra cả điều kiện thứ nhất.
Để giải quyết bài toán này, ta cần tìm hiểu về giao diện của thành phần phần mềm và đặc tả của giao thức và tìm hiểu về phương pháp hình thức để kiểm chứng. Phương pháp mà tôi định sử dụng là kiểm chứng mô hình bằng công cụ kiểm chứng SPIN và đề tài nghiên cứu của chúng tôi là: “Ứng dụng của SPIN để kiểm chứng sự tuân thủ thể thức tương tác của chương trình”. Được biết đề tài này đã được nhiều người nghiên cứu trong và ngoài nước quan tâm, trong tài liệu [13], các tác giả đã xét bài toán này khi giao thức là các ràng buộc về thứ tự các phép toán (không phải là dãy), trong tài liệu [9], tác giả đã đề xuất một mô hình tổng quát và đề xuất các thuật toán để kiểm chứng nhưng các thuật toán này khó cài đặt và không tự động hoàn toàn vì việc kiểm chứng không chỉ đối với giao thức mà cả sự tương thích của dịch vụ thời gian thực nên cần đến các công cụ giải bài toán SAT (Satisfiability – Thỏa mãn của một công thức), tức là các solvers. NỘI DUNG VÀ MỤC ĐÍCH NGHIÊN CỨU Từ việc đặt bài toán và ý tưởng để giải bài toán được đề xuất trên đây, nội dung nghiên cứu của đề tài được xác định như sau.
Tìm hiểu công nghệ phát triển phần mềm hướng thành phần. Tìm hiểu về các thành phần phần mềm trong phần mềm được phát triển theo hướng thành phần với: giao diện của thành phần phần mềm, đặc tả giao thức tương tác của chúng. Trong nội dung này quan trọng là đặc tả giao thức tương tác của các thành phần. Tìm hiểu bộ công kiểm chứng SPIN, ngôn ngữ mô hình hóa Promela trong bộ công cụ SPIN với cách thức mô hình hóa các thể thức tương tác của các thành phần phần mềm trong bộ công cụ SPIN bằng ngôn ngữ Promela.
Trên các cơ sở đó áp dụng bộ công cụ SPIN để kiểm chứng sự tuân thủ thể thức tương tác hoặc không tuân thủ thể thức tương tác của chương trình dựa vào các giao thức tương tác. GIẢ THUYẾT KHOA HỌC Phương pháp kiểm chứng sự tuân thủ hoặc không tuân thể thức tương tác của chương trình bằng công cụ SPIN là cần thiết, nó góp phần tích cực vào việc phát triển phần mềm hướng thành phần bởi nó rất đơn giản, nếu được thực hiện sẽ đảm bảo một thành phần phần mềm sẽ tương thích với chương trình, từ đó giảm LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 8 thời gian phát triển hệ thống, nâng cao chất lượng sản phẩm phần mềm và đáp ứng yêu cầu khách hàng. CẤU TRÚC CỦA LUẬN VĂN Với nội dung nghiên cứu đã nêu ở trên, thì luận văn gồm có các nội dung trình bày như sau: Trình bày về công nghệ phần mềm hướng thành phần. Thành phần phần mềm trong phần mềm được phát triển theo hướng thành phần.
Giao diện tương tác của các thành phần phần mềm. Trong nội dung chủ yếu về công nghệ phần mềm dựa trên thành phần và đặc tả giao thức tương tác của các thành phần. Trình bày về bộ công cụ kiểm chứng mô hình SPIN với ngôn ngữ Promela là ngôn ngữ mô hình hóa trong bộ công cụ SPIN, bài toán deadlock trong SPIN và cách kiểm tra deadlock trong bộ công cụ SPIN. Phần thực nghiệm, áp dụng bộ công cụ SPIN để kiểm chứng sự tuân thủ hoặc không tuân thủ thể thức tương tác của chương trình.
Từ kết quả thực nghiệm này có thể kết luận được phương pháp kiểm chứng đã đưa ra. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 9 CHƯƠNG 2. CƠ SỞ LÝ THUYẾT Nội dung của chương trình bày về công nghệ phần mềm dựa trên thành phần, lợi ích của nó trong phát triển phần mềm. Nghiên cứu, tìm hiểu giao diện tương tác và đặc tả giao thức tương tác của các thành phần trong phần mềm phát triển theo hướng thành phần.
Công nghệ phần mềm dựa trên thành phần Công nghệ phần mềm dựa trên thành phần nhấn mạnh việc thiết kế và xây dựng hệ thống phần mềm dựa trên tái sử dụng các thành phần. Trong công nghệ phần mềm dựa trên thành phần, lập trình viên được giải phóng khỏi các vấn đề chi tiết và nó chuyển trọng tâm từ lập trình tạo phần mềm sang sáng tạo hệ thống. Ngoài ra thì thực hiện tích hợp là trọng tâm. Cơ sở của nó giả định rằng đã có nhiều hệ thống phần mềm lớn, phổ biến để biện minh cho việc khai thác phát triển các thành phần tái sử dụng đáp ứng yêu cầu [3].
Bảo trì hệ thống Yêu cầu Kiểm thử hệ thống Thiết kế hệ thống Tích hợp hệ thống Thiết kế đơn vị Kiểm thử đơn vị Cài đặt Lựa chọn Lắp ghép Kiểm thử Tìm kiếm Đánh giá Hình 2. Tổng quan thiết kế phần mềm dựa trên thành phần Phương pháp phát triển phần mềm dựa trên thành phần dựa trên ý tưởng chọn các thành phần thích hợp có sẵn (off-the-shelf) và sau đó lắp ráp chúng vào một kiến trúc phần mềm đã được xác định. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 10 Công nghệ phần mềm dựa trên thành phần là một nhánh của công nghệ phần mềm, trong đó nhấn mạnh sự tách biệt các mối quan tâm liên quan đến các chức năng mở rộng có sẵn trên toàn hệ thống phần mềm nhất định. Nhằm mục đích mang lại lợi ích trên phạm vi rộng cả ngắn hạn và dài hạn cho bản thân phần mềm và cho các tổ chức bảo trợ phần mềm.
Lịch sử phát triển của công nghệ phần mềm dựa trên thành phần Phát triển phần mềm dựa trên thành phần liên quan đến ý tưởng tái sử dụng (reuse). Ý tưởng về việc tái sử dụng các thành phần trong phần mềm có nguồn gốc từ những năm 1960, ý tưởng trở nên nổi bật tại hội nghị khoa học phần mềm tại Garmisch Đức vào năm 1968 [3] (hội nghị tìm giải pháp khắc phục khủng hoảng phần mềm). Ý tưởng cơ bản đó là: Khi phát triển một hệ thống mới, có thể sử dụng các thành phần đã được phát triển. Khi phát triển các chức năng đặc thù cần thiết trong hệ thống thì cần phát triển theo cách mà chức năng này có thể được sử dụng lại trong các hệ thống khác trong tương lai.
Một số những trường hợp tái sử dụng đầu tiên thành công đó là sự phát triển các thư viện khác nhau, ví dụ như thư viện toán học (sin, cos, ma trận, v. Sự thành công của việc sử dụng lại nằm trong một số cơ sở lập luận: Có cơ sở xác định rõ ràng về các loại chức năng. Giao tiếp giữa các ứng dụng và các chức năng là đơn giản. Các ứng dụng gọi các chức năng gửi cho nó các thông số đầu vào và thư viện đáp ứng bằng cách thực hiện các chức năng và trả lại các kết quả.
Đầu vào và đầu ra được xác định chính xác Xử lý lỗi tốt: nếu đầu vào sai, đầu ra sẽ trả về một giá trị cụ thể thể hiện lỗi. Xây dựng hệ thống dựa trên thành phần 2. Thành phần phần mềm Thành phần phần mềm là gì? Chúng có được quy định, xác định và xử lý không? Để đưa ra một định nghĩa chính xác và hiểu rõ về thành phần thì không phải là dễ dàng. Tuy nhiên có một số định nghĩa, các định nghĩa này cũng phụ thuộc vào nền tảng và sử dụng cho các mục đích khác nhau [6].