zunia.vn

Tuyển sinh 2024 dành cho Gen-Z

zunia.vn

» Công Nghệ Thông Tin

» Kỹ thuật lập trình

Báo cáo môn học các vấn đề hiện đại công nghệ phần mềm

Chia sẻ: Nguyen Tuan Anh | Ngày: | Loại File: DOCX | Số trang:32

Báo xấu

166
lượt xem 22
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Trong các công ty phát triển phần mềm hầu hết công việc kiểm thử của kiểm thử viên được thực hiện thủ công bằng tay. Trong khi đó số lượng tình huống kiểm tra quá nhiều mà các kiểm thử viên không thể hoàn tất bằng tay trong thời gian cụ thể nào đó. Hoặc khi nhóm lập trình đưa ra nhiều phiên bản phần mềm liên tiếp để kiểm tra. Thực tế cho thấy việc đưa ra các phiên bản phần mềm có thể là hàng ngày, mỗi phiên bản bao gồm những tính năng mới, hoặc tính năng...

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Báo cáo môn học các vấn đề hiện đại công nghệ phần mềm

Báo cáo môn học các vấn đề hiện đại công nghệ phần mềm
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. LỜI CẢM ƠN Để hoàn thành báo cáo môn học các vấn đ ề hiện đại công nghệ phần mềm một cách hoàn chỉnh, chúng em xin bày tỏ lòng cảm ơn chân thành đến các thầy cô đ ã hướng dẫn chúng em tại trường Đại Học Công Nghệ. Đặ c biệt là thầyĐặng Đức Hạnh và cô Vũ Diệu Hương, thầ y cô đã trực tiếp hướng dẫ n tận tình, sửa ch ữa và đóng góp nhiều ý kiến quý báu giúp chúng em hoàn thành tốt báo cáo môn học của mình. Lời cảm ơn chân thành và sâu sắc, chúng em xin gửi đ ến gia đình, đ ã luôn sát cánh và động viên chúng em trong những giai đoạn khó khăn nhấ t. Chân thành cảm ơn đến các bạn trong lớp đã hỗ trợ để chúng em có thể hoàn thành tốt công việc được giao. Chúng em xin chân thành biết ơn sự tậ n tình dạy dỗ của tất cả các quý thầy cô Khoa Công nghệ Thông tin – Trường Đại học Công Nghệ Thông Tin – Đại học Quốc gia Hà Nội. Chúng cũng xin chân thành gửi lời cảm ơn đến tất cả các thầy cô đã giảng dạy chúng em thời gian qua, đã truyền đạt và trang bị cho chúng em những kinh nghiệm, kiến thức chuyên môn, giúp chúng em mở rộng tầm nh ìn khi thâm nhập vào thực tế. chúng em xin hứa sẽ không ngừng phấn đấu nỗ lực vươn lên trong học tập và công tác sau này. 2
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. Ph l c LỜI CẢM ƠN ......................................................................................................... 1 CHƯƠNG 1 GIỚI THIỆU ...................................... Error! Bookmark not defined. 1.1Đặt vấn đề ...................................................... Error! Bookmark not defined. 1.2Nộ i dung báo cáo môn học ............................. Error! Bookmark not defined. 1.3Cấu trúc báo cáo môn học .............................. Error! Bookmark not defined. CHƯƠNG 2 TRÌNH BÀY KHÁI NIỆM MÔ HÌNH PROMELA.............................5 Khái niệm cơ bản ngôn ngữ Promela......................................................6 2.1 2.2 Biến và Kiểu ...........................................................................................6 2.3 Định danh, Hằng số và Biểu thức...........................................................7 2.4 Tiến trình.................................................................................................8 2.5 Lệnh và cấu trúc lệnh Promela............................................................... 9 2.6 Sự khác biệt khi sử dụng 2 từ khóa Atomic, D-step trong bài toán cụ thể....................................................................................................................10 CHƯƠNG 3 TRÌNH BÀY CÔNG CỤ SPIN, THAM SỐ, CÚ PHÁP LỆNH.....17 Sơ lược về công c ụ spin...................................................................17 3.1 Lịch sử p hát triển công cụ SPIN..........................................................17 3.2 Một số yếu tố thành công của SPIN......................................................17 3.3 Kiến trúc SPIN – Cấp độ tổ chức Spin.................................................18 3.4 Công cụ dòng lệnh................................................................................18 3.4 CHƯƠNG 4 GIỚ I THIỆU CÔNG CỤ SOẠN TH ẢO EMACS.....................21 4.1 Khái niệm và chức năng của GNU Emacs............................................21 Các lo ại trình soạn thảo Emacs.............................................................22 4.2 Bộ gõ.................................................................................................. ...23 4.4 Giao diện trình so ạn thảo Emacs...........................................................23 4.4 Cấu trúc lệnh Emac...............................................................................24 4.6 Các phím đơn..................................................................................... .24 4.5 3
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. 4.6 Các phím tiền tố và tổ hợp................................................................... 25 CHƯƠNG 5 KẾT LUẬN ....................................... Error! Bookmark not defined. TÀI LIỆU THAM KHẢO....................................... Error! Bookmark not defined. 4
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. CHƯƠNG 1 GIỚ I THIỆU 1.1 Đặt vấn đề Trong các công ty phát triển phần mềm hầu hết công việc kiểm thử của kiểm thử viên được thực hiện thủ công bằng tay. Trong khi đó số lượng tình huố ng kiểm tra quá nhiều mà các kiểm thử viên không thể hoàn tất bằng tay trong thời gian cụ thể nào đó. Hoặc khi nhóm lập trình đưa ra nhiều phiên bản phần mềm liên tiếp để kiểm tra. Thực tế cho thấy việc đưa ra các phiên bản phần mềm có thể là hàng ngày, mỗi phiên bản bao gồm những tính năng mới, hoặc tính năng cũ được sửa lỗi hay nâng cấp. Việc bổ sung hoặc sửa lỗi code cho những tính năng ở phiên bản mới có thể làm cho những tính năng khác đã kiểm tra tốt chạy sai m ặc dù phần code của nó không hề chỉnh sửa. Để khắc phục điều này, đối với từng phiên b ản, kiểm thử viên không chỉ kiểm tra chức năng mới hoặc được sửa, mà phải kiểm tra lại tất cả những tính năng đã kiểm tra tốt trước đó. Điều này khó khả thi về m ặt thời gian nếu kiểm tra thông thường. Để giải quyết vấn đề này chúng ta áp dụng kỹ thuật kiểm thử dựa trên mô hình cho quá trình sinh các ca kiểm thử tự động. Nhưng làm sao đ ể thực hiện được quá trình sinh các ca kiểm thử tự động chúng ta phải áp dụng khá nhiều các công nghệ sẵn có và thông dụng nhất. Ở đây chúng em xin giới thiệu mã nhúng C vào mô tả Promela và trình bày công cụ Spin đ ể sinh ra các ca kiểm thử tự động từ đó áp dụng vào một bài toán cụ thể. Trong báo cáo này chúng em tập trung trình bày về việc nghiên cứu kiểm thử dựa trên mô hình và ứng dụng công cụ Spin vào việc tự động sinh các ca kiểm thử: Xây dựng mô hình hệ thốngvà thực nghiệm. Bên cạnh đó chúng em cũng giới thiệu qua về trình so ạn thảo Emac, một công cụ lập trình khá hay và ra đời từ rất sớm, chạy được trên nhiều hệ điều hành thông dụng. 1.2 Nội dung báo cáo môn họ c 5
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. Bài báo cáo trình bày ngôn ngữ Promela vào thiết kế Promela và áp dụng kĩ thuật sử d ụng công cụ Spin là hai nộ i dung quan trong nhất của quá trình sinh ca kiểm thử tự động. Đề xuất bài toán cụ thể để thực hiện công việc Demo m ột chương trình nhỏ . Từ đó đem áp d ụng vào phục vụ cho việc kiểm chứng phần mềm. Xây dựng tài liệu hướng dẫn về ngôn ngữ Promela, công cụ Spin, trình so ạn thảo Emac phục vụ cho việc nghiên cứu, giảng dậy và ứng d ụng thực tiễn. 1.3 Cấu trúc báo cáo môn học Các phần còn lại của khóa luận có cấu trúc như sau: Chương 2: Trình bày các khái niệm về ngôn ngữ mô hình promela, b ao gồm các đ ịnh nghĩa c ơ b ản về khai báo biến và kiểu, đ ịnh danh, hằng số , biểu thức, tiế n trình. Chương 3: Giới thiệu công cụ Spin, cấu trúc cú pháp lệnh, tham số lệnh và chức năng của nó. Chương 4: Giới thiệu công cụ soạn thảo Emacs. Chương 5: Tóm tắt các kết quả đã đạt được, kết luận, những hạn chế và hướng nghiên cứu phát triển trong tương lai. 6
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. CHƯƠNG 2 TRÌNH BÀY KHÁI NIỆ M MÔ HÌNH PROMELA Chương này sẽ lần lượt trình bày những khái niệm cơ b ản về mô hình Promela. Khái niệm cụ thể về cấu trúc cú pháp lệnh, thủ tục hàm, cách khai báo biến trong Promela. Khái niệm cơ bản ngôn ngữ Promela 2.1 Xây dựng mô hình hệ thống bằng ngôn ngữ Promela là một công đoạn quan trọng trong kiểm thử d ựa trên mô hình, để từ đó có thể dùng công cụ Spin sinh ra các ca kiểm thử. Ngôn ngữ mô hình Promela có nhiều nét tương đồng với ngôn ngữ C.  Định nghĩa Promela (Process meta language ) Promela là ngôn ngữ mô hình dùng đ ể mô tả hệ thống đồ ng thời [The Spin Model Checker: Primer and Reference Manual]. Ví dụ: Giao thức mạng, hệ thống điện thoại, các chương trình giao tiếp đa luồng,…  Cấu trúc chương trình Promela Một chương trình Promela cơ b ản gồm:  K hai báo kiểu.  K hai báo biến.  K hai báo tiến trình.  [init process]. // Các khai báo kiểu và biến mtype = {MSG, ACK}; chan toS = ... chan toR = ... bool flag; // Mộ t tiến trình proctype Sender() { // Thân mộ t tiến trình ... } 7
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. proctype Receiver() { ... } // Tiến trình init init { // Tạo một tiến trình ... } Biến và Kiểu 2.2 Giố ng như nhiều ngôn ngữ lập trình khác, Promela yêu cầu các biến phải được khai báo trước khi chúng có thể được sử dụng. Khai báo biến theo phong cách của ngôn ngữ lập trình C. Theo mặc đ ịnh tất cả các biến của các loại biến cơ bản được bắt đầu từ 0. Cũng như trong C thì 0 được coi như sai và khác 0 được coi là đúng. Một biến có thể là biến toàn cục hoặc là biến địa phương của mỗi tiến trình. Kiểu dữ liệu Kiều Miền giá trị bit or bool { 0, 1} byte 0…255 -2 15 … 215 - 1 short -2 31 … 231 – 1 int • Kiểu khai báo int ii; bit bb; bb = 1; ii = 2; • Kiểu cấu trúc Records (structs): Có th ể tìm ra xung đột khi ch ạy Typedef record{ short f1; b yte f2; } 8
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. Truy cập như C Record rr; rr.f1 = … • Kiểu mảng Một mảng có cấu trúc như sau: int table[max] Lưu ý rằng điều này tạo ra một m ảng max-1 số nguyên: table[0], table[1], ... table[max-1] • Kiểu liệt kê Một bộ các h ằng số tượng trưng được khai báo như sau : mtype = {LINE_CLEAR, TRAIN_ON_LINE, LINE_BLOCKED} • Kênh (Chanel): Được sử d ụng để trao đổi dữ liệu giữa các tiến trình. Cú pháp: chan = [] of ,, ; Cú pháp gửi tin nhắn trong mộ t kênh (!) chan-name ! , ..... ; Cú pháp nhận tin nhắn trong một kênh (?) chan-name ? , .....; Định danh, H ằng số và Biểu thức 2.3 • Định danh Định danh có thể là một chữ cái, một ký tự. • Hằng số Hằng số là một chuỗ i ký tự đại diện cho một số nguyên thập phân. Hằng số tượng trưng có thể được định nghĩa như sau: #define MAX 999 • Biểu thức 9
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. Một biểu thức được xây dựng từ các biến, hằng số và sử dụng các toán tử sau đây: +, -, *, /, %, --, ++, >, >=, ,
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. Tất cả các chương trình promela đều cần một tiến trình init nó giống như hàm main() trong ngôn ngữ C. Việc thực thi một chương trình promela được bắt đầu từ tiến trình init. Một tiến trình init có dạng: init { /* Các khai báo địa phương và các biểu thức. */ } Đơn giản nhất có thể là chương trình promela có dạng: init { skip } Skip có nghĩa là không có biểu thức nào trong tiến trình init; Mỗi tiến trình được định nghĩa bởi một proctype, nó được thực thi đồng thời với tất cả các tiến trình khác, nó giao tiếp với các tiến trình khác thông qua việc sử dụng các biến công cộng hoặc các kênh. Tiến trình thực thi sau khi thực hiện hàm run. Một số ví d ụ đơn giản về tiến trình proctype hello(){ printf("Hello") } proctype world(){ printf("World\n") } init { run hello(); run world () } Lệnh và cấu trúc lệnh Promela 2.5  Mỗi lệnh được ngăn cách với nhau mộ t dấu chấm phẩy (;). Một số lệnh và cấu trúc tiêu biểu • Skip: không thực hiện, chỉ thay đổi khi tiến trình gọi tới • Printf: In ra màn hình. • Assert(Exp) : Sử dụng kiểm tra nếu Exp là biểu thức hợp lệ (Nếu giá trị Exp = 0 thì thực thi sẽ bị lỗ i).  Cấu trúc lặp (do) Cú pháp: if 11
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. :: choice1 -> stat1.1; stat1.2; :: choice2 -> stat2.1; stat2.2; :: .......................................... :: choicen -> statn.1; statn.2; fi; Lựa chọn một trong các điều kiện thực thi  Cấu trúc so sánh (if) do :: choice1 -> stat1.1; stat1.2; :: choice2 -> stat2.1; stat2.2; :: ........................................... :: choicen -> statn.1; statn.2; od; Lựa chọn được lặp đi lặp lại nhiều lần và có thể dừng nếu gặp break.  Cú pháp Active Từ khóa Active có thể là tiền tố cho mọi thủ tục được khai báo trong hàm. Hiệu quả của từ khóa active là tạo ra liên kết Prototype trong hệ thống ban đầu Nhiều trường hợp của cùng một khai báo Prototype có thể được tạo ra bằng cách sử dụng một m ảng các hậu tố tùy chọn. Ví dụ : active [4] proctype hello(){ printf("Hello") } active [7] proctype world(){ printf("World\n") } Lưu ý : trường hợp này sẽ tạo ra 4 trường hợp của “Hello” và 7 trường hợp của “World” 12
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm.  Cú pháp Atomic Có thể sử dụng tới một nhóm lệnh trong một thông báo atomic. Các lệnh được thực hiện đơn lẻ và không xen kẽ với các lệnh trong tiến trình khác. Tự động phá vỡ nếu lệnh bị khóa khi đó các lệnh trong tiến trình khác có thể x en kẽ vào giữa. Cú pháp: atomic { statement1; ...; statementn } Statement1 chạy đầu tiên, statementn chạy cuối cùng.  Cú pháp D -STEP Nhiều phiên bản Atomic : Không chứa trạng thái trung gian được tạo ra và lưu trữ. Chỉ có thể chứa những bước xác đ ịnh. Thời gian chạy sẽ bị lỗ i nếu Stat-I(I>1) bị chặn, khóa. D-STEP cực kì hữu ích để thực hiện việc tính toán trong quá trình chuyển đổi duy nhất. Cú pháp: d-step { statement1; ... ;statementn }  Cú pháp TIME-OUT Lệnh sẽ được thực thi nếu không có một lệnh khác trong các tiến trình khác đang thực thi. Giố ng như thời gian chờ của Hệ thống Spin sử d ụng để giải quyết bế tắc xung đột. Nó không phải là một tính năng thời gian thực và có thể không được sử dụng trong mô hình times-outs tham gia vàothiết kế hệ thống. Sự khác biệt khi sử dụng 2 từ khóa Atomic, D-step trong bài toán cụ 2.6 thể  Mô hình o K hi không sử dụng từ khóa trong chương trình 13
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. Hình 1: Khi không sử dụng từ khóa Các trạng thái sinh ra khi không sử d ụng từ khóa sẽ được tăng lên theo công bội. Trong trường hợp này tất cả các trạng thái có thể tạo được từ chương trình đ ều có thể sinh ra. Do đó những trạng thái không cần thiết mà vẫn được lưu trữ trong bộ nhớ sẽ làm lãng phí mộ t phần bộ nhớ và số lượng trạng nhiều như vậy sẽ làm cho người thiết kế khó có thể kiểm soát được. o K hi sử dụng từ khóa Atomic 14
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. Hình 2: khi sử dụng từ khóa Atomic Mặc dù câu lệnh Atomic sẽ không được chạy xen kẽ nhau nhưng các trạng thái trung gian vẫn sẽ được khởi tạo và lưu trữ trong stack. Do đó khi có một trạng thái trung gian (trạng thái A) bị khóa , ngắt thì lời gọi Atomic sẽ bị m ất và các trạng thái trung gian sẽ được đến thăm. o K hi sử dụng từ khóa D-STEP 15
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. Hình 3: khi sử dụng từ khóa D-Step Khác với từ khóa Atomic, từ khóa D-Step thực thi mộ t mã lênh nếu một bước hay giao dịch nào bị khóa thì chương trình sẽ bị lỗi. Các trạng thái trung gian sẽ không được khởi tạo.  Một chương trình đ ơn giản để kiểm tra chức năng khi sử dụng các từ khóa o Mã lệnh: Khi không sử dụng từ khóa nào. 16
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. int x=0 int y=0;int z=0 proctype A(){ printf("gia tri x1= %d \n", 1); printf("gia tri y1= %d \n", 1); printf("gia tri z1= %d\n", 1); } proctype B(){ printf("gia tri x2= %d \n", 2); printf("gia tri y2= %d \n", 2); printf("gia tri z2= %d\n", 2); } init { run A(); run B(); } Hình 4: Chương trình không sử dụng lệnh Atomic, D-step Khi không sử dụng từ khóa nào thì số các trạng thái sinh ra trong ví dụ trên sẽ là 9 trường hợp. Do các câu lệnh trong hai tiến trình sẽ chạy xen kẽ với nhau. o Mã lệnh: Khi sử dụng từ khóa atomic hoặc D -step Do chức năng của mã lệnh atomic và D-step là tương đối giống nhau chỉ khác nhau đôi chút về trạng thái trung gian được khởi tạo. Atomic : Khởi tạo trạng thái trung gian nhưng chỉ lưu vào stack. Cho đến khi nào có mộ t trạng thái bên trong mã lệnh atomic bị khóa, ngắt thì mới thực hiện các trạng thái trong Stack. D -step: Không khởi tạo trạng thái trung gian nên khi có một trạng thái nào bên trong mã lệnh D-step bị khóa thì chương trình thực thi sẽ bị lỗi. 17
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. int x=0 int y=0; int z=0 proctype A(){ atomic{ printf("gia tri x1= %d \n", 1); printf("gia tri y1= %d \n", 1); printf("gia tri z1= %d\n", 1); } } proctype B(){ printf("gia tri x2= %d \n", 2); printf("gia tri y2= %d \n", 2); printf("gia tri z2= %d\n", 2); } init { run A(); run B(); } Hình 5: Khi sử dụ ng từ khóa Atomic, D-step Trong trường hợp này thì số các trạng thái sinh ra sẽ giảm đi bởi vì khi bắt đầu đ ến trạng thái x1 thì chương trình phải chạy hết đến trạng thái x3 rồi mới xen kẽ tới các trạng thái khác được. Dựa vào đặc điểm này mà người kiểm thử có thể loại bớt đi được khá nhiều các trạng thái không cần thiết. 18
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. CHƯƠNG 3 TRÌNH BÀY CÔNG CỤ SPIN, THAM SỐ , CÚ PHÁP LỆNH Sơ lược về công c ụ spin 3.1 SPIN là công cụ mã nguồ n mở, phổ biến và được sử dụng bởi hàng ngàn người trên toàn cầu. SPIN được sử dụng cho việc xác minh thẩm định của các hệ thống phân phối phần mềm. Nó cung cấp một giả lập cho phép các nhà thiết kế đ ạt được kết quả phản hồ i từ hệ thống mô hình của họ. Những kết quả p hản hồi đó đóng vai trò quan trọng trong sự hiểu biết của các nhà thiết kế về hệ thố ng trước khi họ đầu tư vào phân tích chính thức. Lịch sử p hát triển công cụ SPIN 3.2 Từ năm 1980 Spin được phát triển tại Bell Labs của nhóm Unix Phần mềm này phát triển rộng rãi từ năm 1991. Tháng 4 năm 2002 Spin được trao giải thưởng phần mềm uy tín cho năm 2001 của ACM. Các version chính: năm 1991 là 1.0 (initial version) tới năm 2002 đ ã có SPIN version 4.0 (automata extration from C code). 1.0 Jan 1991 Initial version (Holzmann 1991 2.0 Jan 1995 Partial order reduction 3.0 Apr 1997 Minimised automaton representation 4.0 Late 2002 Ax: automata extraction from C code 5.0 Oct 2007 Multi-core & swarm support 6.0 Dec 2010 Inline LTL formula parallel bfs Một số yếu tố thành công của SPIN 3.3 Cú pháp thực hiện (bằng cách sử dụng tựa ngôn ngữ C). Giao diện người dùng đồ họa đẹp Xspin. 19
Bộ môn : Các vấn đề hiện đại công nghệ phần mềm. Không chỉ là một công cụ nghiên cứu, mà còn là công cụ hỗ trợ. Chứa nhiều hơn so với nhiều thập kỷ nghiên cứu kéo xác minh máy tính tiên tiến AIDEC (nhiều thuật toán tối ưu hóa). Kiến trúc SPIN – Cấp độ tổ chức Spin 3.4 Hình 6: Cấp độ tổ chức SPIN Công cụ dòng lệnh. 3.4 3.4.1 Cú pháp Spin Một số câu lênh trong SPIN. Spin –a [-m] [-Pcpp] file spin [-bglmprsv] [-J] [-qN] [-nN] [-Pcpp] file spin -c [-t] [-Pcpp] file spin -d [-Pcpp ] file spin -f LTL spin -F file spin -i [-bglmprsv] [-J] [-qN] [-Pcpp] file 20

CÓ THỂ BẠN MUỐN DOWNLOAD

THÔNG TIN

TRỢ GIÚP

HỖ TRỢ KHÁCH HÀNG

Theo dõi chúng tôi

Chịu trách nhiệm nội dung:

Nguyễn Công Hà - Giám đốc Công ty TNHH TÀI LIỆU TRỰC TUYẾN VI NA

LIÊN HỆ

Địa chỉ: P402, 54A Nơ Trang Long, Phường 14, Q.Bình Thạnh, TP.HCM

Hotline: 093 303 0098

Email: support@tailieu.vn

Giấy phép Mạng Xã Hội số: 670/GP-BTTTT cấp ngày 30/11/2015 Copyright © 2022-2032 TaiLieu.VN. All rights reserved.