- Phương pháp tạo giả định tối thiểu áp dụng để kiểm chứng phần mềm hướng thành phẩm. - Luận văn Thạc sĩ ngành: Công nghệ phần mềm. - Abstract: Giới thiệu tổng quan phần mềm hướng thành phần, đưa ra các khái niệm cơ bản và cách tiếp cận để kiểm chứng phần mềm hướng thành phần. - Trình bày chi tiết thuật toán học L*, giải thuật tạo giả định sử dụng thuật toán học L*. - Nghiên cứu giải thuật tạo giả định tối thiểu. - Đưa ra một phản ví dụ để minh hoạ rằng: giả định được tạo ra bởi giải thuật sử dụng thuật toán học L* chưa phải là giả định tối thiểu. - Nêu lên một ví dụ cụ thể để minh hoạ cho thuật toán tạo giả định tối thiểu. - Sử dụng bộ công cụ LTSA để xác minh một số hệ thống đơn giản nhằm so sánh về thời gian cũng như bộ nhớ sử dụng của giải pháp cũ và giải pháp được đưa ra trong luận văn.. - Keywords: Công nghệ phần mềm. - Phần mềm hướng thành phẩm. - Phát triển phần mềm hướng thành phần (Component-Based Software Development - CBSD) là một trong những công nghệ quan trọng nhất trong kỹ nghệ phần mềm. - Hệ thống phần mềm hướng thành phần được xây dựng dựa trên quá trình lựa chọn và ghép nối các thành phần riêng biệt thành một hệ thống hoàn chỉnh. - Với cách tiếp cận này, phát triển phần mềm hướng thành phần đã góp phần rút ngắn thời gian thực hiện dự án, nâng cao chất lượng và độ tin cậy của sản phầm. - Vì những ưu điểm này mà công nghệ này đã được áp dụng rộng rãi trong quá trình phát triển các dự án phần mềm hiện nay. - Tuy nhiên, một trong những hạn chế của CBSD là vấn đề đảm bảo tính đúng đắn của hệ thống khi ghép nối các thành phần với nhau vì các thành phần có thể được phát triển một cách độc lập hoặc được đặt mua từ các công ty thứ 3 (third parties). - Hiện tại, các công nghệ hỗ trợ phát triển phần mềm hướng thành phần như CORBA (OMG), COM/DCOM or .NET (Microsoft), Java and JavaBeans (Sun. - vv chỉ hỗ trợ việc ghép nối các thành phần (component plugging). - kiểm tra liệu các thành phần có thể bị lỗi khi cộng tác với nhau hay không. - Một trong những giải pháp phổ biến để giải quyết vấn đề nêu trên là sử dụng các phương pháp kiểm chứng mô hình (Model checking). - Tuy nhiên, một trong những hạn chế lớn nhất của kiểm chứng mô hình là vấn đề bùng nổ không gian trạng thái khi kiểm chứng các phần mềm có kích thước lớn. - Một trong những cách tiếp cận tiềm năng để giải quyết vấn đề này là áp dụng kiểm chứng từng phần (modular verification - MV). - Thay vì tiến hành kiểm chứng trên toàn bộ hệ thống gồm các thành phần được ghép nối với nhau, cách tiếp cận này tiến hành kiểm chứng trên từng thành phần riêng biệt. - Một trong những phương pháp kiểm chứng hỗ trợ ý tưởng này là phương pháp kiểm chứng đảm bảo giả định (Assume-Guarantee Verification - AGV). - Sử dụng tư tưởng của chiến lược “chia để trị”, AGV phân chia bài toán kiểm chứng thành các bài toán con cùng dạng nhưng kích thước nhỏ hơn sao cho chúng ta có thể kiểm chứng các bài toán con một cách riêng biệt. - AVG được đánh giá là một phương pháp hứa hẹn để kiểm chứng phần mềm hướng thành phần thông qua phương pháp kiểm chứng mô hình. - AVG không những thích hợp cho phần mềm hướng thành phần mà còn có khả năng giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm chứng mô hình. - Trong phương pháp này, các giả định (assumptions) (có vai trò như là môi trường của các thành phần) sẽ được tạo lập. - Việc tạo lập các giả định chính là bài toán quan trọng nhất trong phương pháp này. - Kích thước của các giả định này (số lượng trạng thái) nên được cực tiểu hóa bởi vì chi phí cho quá trình kiểm chứng mô hình của phương pháp này phụ thuộc chính vào thông số này. - Với mục tiêu này, chúng tôi đề xuất một phương pháp tạo giả định tối thiểu (có kích thước nhỏ nhất) như là một cải tiến của phương pháp kiểm chứng đảm bảo giả định như đã trình bày ở trên. - Ý tưởng chính của phương pháp đề xuất là tìm kiếm giả định tối thiểu trên toàn bộ không gian tìm kiếm của các ứng cử viên giả định (candidate assumptions). - Giả định tối thiểu sau khi tạo lập bằng phương pháp đề xuất sẽ được sử dụng để kiểm chứng lại hệ thống với chi phí thấp hơn. - Chương 1: Giới thiệu tổng quan phần mềm hướng thành phần, các khái niệm cơ bản, cách tiếp cận để kiểm chứng phần mềm hướng thành phần.. - Chương 2: Trình bày chi tiết thuật toán học L. - giải thuật tạo giả định sử dụng thuật. - Chương 3: Chương này trình bày giải thuật tạo giả định tối thiểu. - Trong chương này chúng tôi sẽ đưa ra một phản ví dụ để minh hoạ rằng: giả định được tạo ra bởi giải thuật sử dụng thuật toán học L* chưa phải là giả định tối thiểu. - Chúng tôi cũng sẽ trình bày một ví dụ cụ thể để minh hoạ cho thuật toán tạo giả định tối thiểu.. - Chúng tôi sử dụng bộ công cụ LTSA để xác minh một số hệ thống đơn giản nhằm so sánh về thời gian cũng như bộ nhớ sử dụng của giải pháp cũ và giải pháp được đưa ra trong luận văn.. - [2] C.Blundell, D.Griannakaopoulou, C.Pasareanu: “assume-Guanrantee Testing”, Microsoft Research – Specification and Verification of Component-Based Systems (SAVCBS2005) Worshop :7-14. - Cerna, P.Varekova : “Component-Interaction Automata as a Verification-Oriented Component-Based System Specification”, Microsoft Research – Specification and Verification of Component-Based Systems(SAVCBS 2005) Workshop : 3138.. - Fisler and S.Krishnamurthi : “Modular verification of collaboration-based software designs”, In Proc. - Cobleigh: “Assume-Guarantee Verification of Source Code with Design-Level Assumptions”, ICSE . - Keller: “Formal verification of parallel programs”, Communications of the ACM July 1976.. - Vardi: “Modular model checking”, In Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science. - Katayama: “Open Incremental Model Checking”, Microsoft Research - Specification and Verification of Component-Based Systems (SAVCBS) Workshop, ACM FSE’04.. - Katayama: “A Formal Approach Facilitating the Evolution of Component-Based Software”, IEEE Computer Proc. - Katayama: “Specification and Verification of Inter-Component onstraints in CTL”, Microsoft Research - Specification and Verification of Component- Based Systems (SAVCBS) Workshop, ACM SIGSOFT ESEC/FSE’05.. - Huth: “Assume-guarantee model checking of software: A comparative case study”, In Theoretical and Practical Aspects of SPIN. - Katayama: “An Assume-Guarantee Method for Modular Verification of Evolving Component-Based Software”, In Supplemental Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2007. - Katayama: Modular Conformance Testing and Assume- Guarantee Verification for Evolving Component-Based Software