Tài liệu ứ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 (tt)

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ HOÀNG VĂN THỦY Ứ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 LUẬN VĂN THẠC SỸ CÔNG NGHỆ THÔNG TIN Hà Nội – 2014 2 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ HOÀNG VĂN THỦY Ứ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 Ngành: Công nghệ thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 60480103 LUẬN VĂN THẠC SỸ CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: TIẾN SĨ ĐẶNG VĂN HƯNG Hà Nội – 2014 3 LỜI CẢM ƠN Trước hết tôi xin bày tỏ lòng biết ơn sâu sắc và gửi lời cảm ơn đặc biệt nhất tới Thầy TS. Đặng Văn Hưng, người đã định hướng đề tài, cung cấp cho tôi những kiến thức, những tài liệu và tận tình hướng dẫn chỉ bảo tôi trong suốt quá trình thực hiện đề tài luận văn cao học này, từ những ý tưởng trong đề cương nghiên cứu, phương pháp nghiên cứu, phương pháp giải quyết vấn đề cho đến những lần kiểm tra cuối cùng để hoàn thành luận văn này. Tôi xin bày tỏ lòng biết ơn chân thành tới Thầy, Cô giáo trong bộ môn Kỹ thuật phần mềm, Khoa Công nghệ thông tin, những người đã mang trí tuệ, công sức truyền đạt giúp tôi mở rộng kiến thức về Công nghệ thông tin nói chung và Kỹ thuật phần mềm nói riêng, đó là những kiến thức quý báu và sẽ rất có ích với tôi trong giai đoạn hiện tại và tương lai. Tôi xin gửi lời cảm ơn chân thành tới Ban Giám hiệu Nhà trường, Phòng Đào tạo sau đại học, Đại học Công nghệ - Đại học Quốc gia Hà Nội đã tạo điều kiện tốt nhất giúp tôi trong suốt quá trình học tập. Cuối cùng tôi xin gửi lời cảm ơn đến gia đình, bạn bè những người đã luôn động viên khuyến khích tôi trong suốt quá trình học tập cũng như thực hiện đề tài luận văn của mình. Hà Nội, ngày 08 tháng 11 năm 2014 Học viên Hoàng Văn Thủy 4 5 LỜI CAM ĐOAN Tôi xin cam đoan nội dung trình bày trong luận văn này là do tôi tự nghiên cứu tìm hiểu dựa trên các tài liệu và tôi trình bày theo ý hiểu của bản thân dƣới sự hƣớng dẫn trực tiếp của Thầy TS. Đặng Văn Hƣng. Các nội dung nghiên cứu, tìm hiểu và kết quả thực nghiệm là hoàn toàn trung thực. Luận văn này của tôi chƣa từng đƣợc ai công bố trong bất cứ công trình nào. Trong quá trình thực hiện luận văn này tôi đã tham khảo đến các tài liệu của một số tác giả, tôi đã ghi rõ tên tài liệu, nguồn gốc tài liệu, tên tác giả và tôi đã liệt kê trong mục “DANH MỤC TÀI LIỆU THAM KHẢO” ở cuối luận văn. Học viên Hoàng Văn Thủy 6 7 MỤC LỤC LỜI CẢM ƠN ............................................................................................................................... 1 LỜI CAM ĐOAN ......................................................................................................................... 5 MỤC LỤC .................................................................................................................................... 7 DANH MỤC HÌNH VẼ................................................................................................................ 9 DANH MỤC BẢNG..................................................................................................................... 9 CHƢƠNG 1. MỞ ĐẦU .............................................................................................................. 10 1.1. ĐẶT VẤN ĐỀ ................................................................................................................. 10 1.2. NỘI DUNG VÀ MỤC ĐÍCH NGHIÊN CỨU ................................................................ 11 1.3. GIẢ THUYẾT KHOA HỌC ........................................................................................... 12 1.4. CẤU TRÚC CỦA LUẬN VĂN ...................................................................................... 12 CHƢƠNG 2. CƠ SỞ LÝ THUYẾT ............................................Error! Bookmark not defined. 2.1. Công nghệ phần mềm dựa trên thành phần ......................Error! Bookmark not defined. 2.2. Lịch sử phát triển của công nghệ phần mềm dựa trên thành phần .......... Error! Bookmark not defined. 2.3. Xây dựng hệ thống dựa trên thành phần ...........................Error! Bookmark not defined. 2.3.1. Thành phần phần mềm ...............................................Error! Bookmark not defined. 2.3.2. Xác định thành phần ..................................................Error! Bookmark not defined. 2.3.2.1. Dùng lại ............................................................... Error! Bookmark not defined. 2.3.2.2. Phát triển mới ......................................................Error! Bookmark not defined. 2.3.2.3. Thích nghi ...........................................................Error! Bookmark not defined. 2.3.2.4. Cập nhật thành phần............................................Error! Bookmark not defined. 2.4. Lợi ích của công nghệ phần mềm dựa trên thành phần ....Error! Bookmark not defined. 2.6. Mô hình hóa giao diện thành phần ...................................Error! Bookmark not defined. 2.6.1. Giao diện ....................................................................Error! Bookmark not defined. 2.6.2. Vai trò giao diện.........................................................Error! Bookmark not defined. 2.6.3. Đặc tả giao diện với một số ngôn ngữ cơ sở ..............Error! Bookmark not defined. 2.6.4. Đặc tả giao diện với các ràng buộc cơ sở ..................Error! Bookmark not defined. 2.7. Kết luận .............................................................................Error! Bookmark not defined. CHƢƠNG 3. BỘ CÔNG CỤ KIỂM CHỨNG MÔ HÌNH SPIN VÀ BÀI TOÁN DEADLOCK ......................................................................................................Error! Bookmark not defined. 3.1. Kiểm duyệt mô hình..........................................................Error! Bookmark not defined. 3.1.1. Tổng quan hoạt động của kiểm duyệt mô hình ..........Error! Bookmark not defined. 3.1.2. Quá trình hoạt động của kiểm duyệt mô hình ............Error! Bookmark not defined. 3.1.3. Ƣu, nhƣợc điểm của kiểm duyệt mô hình.....................Error! Bookmark not defined. 3.2. Bộ công cụ SPIN ............................................................... Error! Bookmark not defined. 3.2.1. Tổng quan về SPIN ....................................................Error! Bookmark not defined. 3.2.2. Cấu trúc của SPIN ......................................................Error! Bookmark not defined. 3.2.3. Công cụ ISPIN ...........................................................Error! Bookmark not defined. 3.3. Ngôn ngữ Promela ............................................................Error! Bookmark not defined. 3.3.1. Tổng quan về Promela ...............................................Error! Bookmark not defined. 3.3.2. Chƣơng trình Promela ...............................................Error! Bookmark not defined. 3.3.3. Tiến trình ....................................................................Error! Bookmark not defined. 3.3.4. Tiến trình Init và Run .................................................Error! Bookmark not defined. 3.3.5. Biến trong Promela ....................................................Error! Bookmark not defined. 3.3.6. Kiểu dữ liệu trong Promela .......................................Error! Bookmark not defined. 8 3.3.6.1. Kiểu dữ liệu cơ bản ..............................................Error! Bookmark not defined. 3.3.6.2. Kiểu dữ liệu có cấu trúc .......................................Error! Bookmark not defined. 3.3.7. Toán tử, dịnh danh, hằng và biểu thức .......................Error! Bookmark not defined. 3.3.8. Câu lệnh trong Promela .............................................Error! Bookmark not defined. 3.3.9. Các cấu trúc điều khiển ..............................................Error! Bookmark not defined. 3.3.9.1. Câu lệnh điều kiện IF ...........................................Error! Bookmark not defined. 3.3.9.2. Câu lệnh lặp DO ..................................................Error! Bookmark not defined. 3.3.10. Đan xen (interleaving) .............................................Error! Bookmark not defined. 3.3.11. Cấu trúc atomic ........................................................Error! Bookmark not defined. 3.3.12. Kênh trong Promela .................................................Error! Bookmark not defined. 3.3.12.1. Biến kênh ...........................................................Error! Bookmark not defined. 3.3.12.2. Kênh gặp (rendezvous) ......................................Error! Bookmark not defined. 3.3.12.3. Kênh đệm (Buffer) .............................................Error! Bookmark not defined. 3.4. Bài toán deadlock trong SPIN ...........................................Error! Bookmark not defined. 3.5. Kết luận .............................................................................Error! Bookmark not defined. CHƢƠNG 4. KIỂM CHỨNG SỰ TUÂN THỦ THỂ THỨC TƢƠNG TÁC CỦA CHƢƠNG TRÌNH BẰNG SPIN ...................................................................Error! Bookmark not defined. 4.1. Phƣơng pháp .....................................................................Error! Bookmark not defined. 4.2. Áp dụng.............................................................................Error! Bookmark not defined. 4.3. Kết luận .............................................................................Error! Bookmark not defined. CHƢƠNG 5. KẾT LUẬN VÀ HƢỚNG PHÁT TRIỂN .............Error! Bookmark not defined. 5.1. Kết luận .............................................................................Error! Bookmark not defined. 5.2. Hƣớng phát triển. ..............................................................Error! Bookmark not defined. DANH MỤC TÀI LIỆU THAM KHẢO .................................................................................... 13 PHỤ LỤC.....................................................................................Error! Bookmark not defined. 9 DANH MỤC HÌNH VẼ Hình 2.1. Tổng quan thiết kế phần mềm dựa trên thành phần ................................ 9 Hình 2.2. Kiến trúc hệ thống của phần mềm hƣớng thành phần ......................... 11 Hình 2.3. Mô hình phát triển phần mềm dựa trên thành phần .............................. 14 Hình 2.4. Mô hình truyền thông............................................................................ 22 Hình 3.1. Sơ đồ tổng quan của kiểm duyệt mô hình ............................................ 29 Hình 3.2. Cấu trúc mô hình kiểm chứng SPIN ..................................................... 32 Hình 3.3. Giao diện ISPIN soạn thảo mã nguồn mô hình kiểm chứng ..................... 33 Hình 3.4. Thiết lập thông số khi thực hiện Simulate/Replay. ..................................... 34 Hình 3.5. Thiết lập thông số Verification để kiểm chứng. ......................................... 34 Hình 3.6. Mô hình gửi và nhận thông điệp trên kênh gặp (rendezvous) .............. 47 Hình 3.7. Mô hình gửi và nhận thông tin trên kênh đệm (Buffer) ....................... 47 Hình 3.8. Báo cáo deadlock và vi phạm của chƣơng trình guinhan ..................... 50 Hình 4.1 Automat mô tả giao thức của thành phần quản lý cơ sở dữ liệu. .................. 52 Hình 4.2 Automat mô tả giao thức tƣơng tác của thành phần môi trƣờng có biểu thức chính quy là or*w*ct ..................................................................................... 55 Hình 4.3 Automat mô tả thể thức của thành phần môi trƣờng có biểu thức chính quy là or*w*rct. .................................................................................................... 55 Hình 4.4 Automat thể hiện các trạng thái của tiến trình pro. ............................... 57 Hình 4.5 Automat thể hiện các trạng thái của tiến trình user1. ............................ 58 Hình 4.6. Kết quả khi chạy mô phỏng tƣơng tác giữa pro và user1 ..................... 58 Hình 4.7. Kết quả sau khi Run verification (thể hiện sự tuân thủ thể thức tƣơng tác của chƣơng trình sau khi chạy mô phỏng trên ISPIN) .......................................... 59 Hình 4.8 Automat thể hiện các trạng thái của tiến trình user2. ............................ 60 Hình 4.9. Kết quả khi chạy mô phỏng tƣơng tác giữa pro và user2 ..................... 60 Hình 4.10. Kết quả sau khi Run verification (thể thức của thành phần không tuân thủ thể thức của chƣơng trình sau khi chạy mô phỏng trên ISPIN). .................... 61 DANH MỤC BẢNG Bảng 3.1 Kiểu dữ liệu cơ bản ............................................................................... 38 Bảng 3.2. Toán tử trong Promela .......................................................................... 39 Bảng 3.3. Bảng thể hiện xen kẽ trạng thái của chƣơng trình Promela PQ ........... 44 Bảng 3.4. Kết quả đầu ra có thể của chƣơng trình Promela PQ ........................... 44 10 CHƯƠNG 1. MỞ ĐẦU 1.1. ĐẶ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. 11 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 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. 1.2. 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. 12 1.3. 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 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. 1.4. 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. 13 DANH MỤC TÀI LIỆU THAM KHẢO [1]. Andrew Ireland Department of Computer Science School of Mathematical and Computer Sciences Heriot-Watt University Edinburgh, “Distributed Systems Programming (F21DS1) Promela I”. [2]. Mordechai Ben-Ari (2008), Principles of the Spin Model Checker, SpringerVerlag, London. [3]. Debayan Bose (2010), “Component Based Development”, Indian Statistical Instute. [4]. Xia Cai, Michael R. Lyu, Kam-Fai Wong, Roy Ko (2001), “Component-Based Software Engineering: Technologies, Development Frameworks, and Quality Assurance Schemes”, The Chinese University of Hong Kong. [5]. Divya Chaudhary (2013), “Component Based Software Engineering Systems: Process and Metrics”, International Journal of Advanced Research in Computer Science and Software Engineering, Vol. 3, No. 2277. [6]. Ivica Crnkovic, Magnus Larsson, “Component-Based Software Engineering – New Paradigm of Software Development”, Department of Computer Engineering Malardalen University. [7]. Jun Han (2001), “Temporal Logic Based Specification of Component Interaction Protocols”, School of Network Computing Monash University, McMahons Road Frankston, Australia. [8]. Jun Han (2000), “Rich Interface Specication for Software Components”, Peninsula School of Computing and Information Technology Monash University, McMahons Road Frankston, Australia. [9]. Truong Anh Hoang, Trinh Thanh Binh, Dang Van Hung, Nguyen Viet Ha, Nguyen Thi Thu Trang, Pham Dinh Hung (2008), “Checking Interface Interaction Protocols Using Aspect-Oriented Programming”, SEFM, pp. 382-386. [10]. Gerard J. Holzmann (1997), “The Model Checker SPIN”, IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, Vol. 23, No. 5, pp. 1-2. 14 [11]. Dang Van Hung, “Some Advanced Topics on Software Engineering”, Lectures in College of Technology. [12]. Dang Van Hung, “Model-Checking and the SPIN Modelchecker”, Lectures. [13]. Dang Van Hung and Truong Anh Hoang (2013), “Modeling and Specification of Real-Time Interfaces with UTP”, Theories of Programming and Formal Methods, Springer, pp. 136-150. [14]. Christel Baier Joost-Pieter Katoen (2008), Principles of Model Checking, The MIT Press Cambridge, Massachusetts London, England. [15]. Ehsan Kouroshfar, Hamed Yaghoubi Shahir and Raman Ramsin, “Process Patterns for Component-Based Software Development”, Department of Computer Engineering Sharif University of Technology. [16]. Jani Lampinen, Sami Liedes, Kari Kahkonen, Janne Kauttio, and Keijo Heljanko (2009), “INTERFACE SPECIFICATION METHODS FOR SOFTWARE COMPONENTS”, Espoo TKK Reports in Information and Computer Science. [17]. Bertrand Meyer (1997), Object-oriented Software Construction, ISE Inc Santa Barbara California. [18]. Taraq Hussain Sheakh (2014), “Software Reliability Analysis- A new Approach”, International Journal of Scientific Research, Vol. 3, No. 2277, pp. 75-76. [19]. http://spinroot.com.