Báo cáo Đặc tả và kiểm chứng thiết kế của hệ thống tương tranh

Trình bày các kiến thức cơ bản liên quan đến đặc tả và kiểm chứng thiết kế của Hệ thống tương tranh gồm: Máy hữu hạn trạng thái, máy dịch chuyển trạng thái có gán nhãn và công cụ hỗ trợ kiểm chứng Điều khiển các hành động trong mô hình (LTSA). Nghiên cứu một kỹ thuật phát hiện lỗi của chương trình tương tranh bằng cách sử dụng khả năng mô phỏng của công cụ LTSA, từ đó phát hiện ra các sai sót của hệ thống. Trình bày chi tiết phương pháp đặc tả và kiểm chứng hệ...
Nội dung trích xuất từ tài liệu:
Báo cáo "Đặc tả và kiểm chứng thiết kế của hệ thống tương tranh " Đặc tả và kiểm chứng thiết kế của hệ thống tương tranh Hoàng Phương Thức Trường Đại học Công nghệ Luận văn ThS. ngành: Công nghệ phần mềm; Mã số: 60 48 10 Người hướng dẫn: TS. Phạm Ngọc Hùng Năm bảo vệ: 2011 Abstract. Trình bày các kiến thức cơ bản liên quan đến đặc tả và kiểm chứng thiết kế của Hệ thống tương tranh gồm: Máy hữu hạn trạng thái, máy dịch chuyển trạng thái có gán nhãn và công cụ hỗ trợ kiểm chứng Điều khiển các hành động trong mô hình (LTSA). Nghiên cứu một kỹ thuật phát hiện lỗi của chương trình tương tranh bằng cách sử dụng khả năng mô phỏng của công cụ LTSA, từ đó phát hiện ra các sai sót của hệ thống. Trình bày chi tiết phương pháp đặc tả và kiểm chứng hệ thống tương tranh và việc sử dụng công cụ LTSA để hỗ trợ mục đích này, và đưa ra một ví dụ minh họa về hệ thống quan sát số người trong siêu thị để minh họa cho các nghiên cứu của luận văn. Keywords. Công nghệ phần mềm; Kiểm thử phần mềm; Hệ thống tương tranhContent Đảm bảo chất lượng phần mềm (Software Quality Assurance - SQA) [2] là một phaquan trọng trong quá trình phát triển phần mềm. SQA đang là vấn đề nhận được sự quan tâmcủa cộng đồng nghiên cứu và hầu hết các công ty phần mềm. Ở mức cao, việc đảm bảo chấtlượng liên quan đến một loạt các vấn đề như chuẩn và quy trình quản lý của công ty, môitrường và công cụ phát triển, mô hình phát triển phần mềm được lựa chọn, kỹ năng của nhânviên,… Ở mức trực tiếp hơn, chất lượng phần mềm được đảm bảo trên cơ sở hiểu đúng yêucầu của khách hàng, đặc tả đúng yêu cầu, tạo ra các thiết kế tốt và chuyển nó thành mã nguồncủa phần mềm một cách đúng đắn. Do đó việc đảm bảo chất lượng phần mềm là rất khó khănvà tốn kém. Các công ty phần mềm lớn luôn có một bộ phận đặc trách về vấn đề đảm bảochất lượng phần mềm. Trong quá trình phát triển phần mềm, kiểm thử phần mềm (software testing) [6] đangđược sử dụng như là một giải pháp chủ yếu nhằm đảm bảo chất lượng phần mềm. Kiểm thửphần mềm là một chiến lược gồm nhiều bước với một loạt phương pháp thiết kế các ca kiểmthử (test cases) nhằm phát hiện ra lỗi hoặc khiếm khuyết của phần mềm. Tuy nhiên, kiểm thửchỉ có thể phát hiện ra lỗi hoặc khiếm khuyết của phần mềm chứ không chỉ ra được phầnmềm không còn lỗi. Đối với các hệ thống đòi hỏi tính đúng đắn cao như hệ thống điều khiển,hệ thống nhúng,… kiểm thử là không đủ để đảm bảo được chất lượng của các hệ thống này.Hiện nay, rất nhiều khách hàng hoặc chủ đầu tư đã yêu cầu đơn vị phát triển phải áp dụng cácphương pháp kiểm chứng (software verification) [8] để chứng minh tính đúng đắn của hệthống trước khi đưa vào triển khai. Các phương pháp kiểm chứng hiện tại chỉ tập trung vào việc chứng minh tính đúngđắn của chương trình/cài đặt nhằm phát hiện các lỗi lập trình so với thiết kế. Để thực hiệnđược điều này, chúng ta phải giả sử rằng thiết kế của phần mềm là đúng. Giả thiết này khôngthực tế vì các thiết kế, đặc biệt là thiết kế các hệ thống lớn thường có lỗi. Vì vậy, vấn đề đảmbảo tính đúng đắn của thiết kế trước khi tiến hành cài đặt có ý nghĩa quan trọng nhằm nângcao độ tin cậy và chất lượng phần mềm, nó là một nhân tố không thể thiếu trong việc đảmbảo chất lượng phần mềm. Thật vậy, nếu chúng ta không đảm bảo được điều này thì khichương trình có lỗi xảy ra, chúng ta sẽ không biết được lỗi là do thiết kế hay do cài đặt. Điềunày tiêu tốn rất nhiều tài nguyên, công sức và chi phí để phát hiện ra lỗi của chương trình.Ngược lại, nếu chúng ta đảm bảo được rằng thiết kế đã đúng trước khi tiến hành cài đặt sẽgiúp cho chúng ta sớm phát hiện ra lỗi thiết kế. Việc phát hiện sớm các lỗi thiết kế trước khicài đặt sẽ giảm đáng kể chi phí trong sản xuất phần mềm. Hơn nữa, một khi thiết kế đã đượcchứng minh là đúng thì khi chương trình có lỗi, chúng ta có thể kết luận rằng đấy là lỗi lậptrình. Mục đích của luận văn là nghiên cứu phương pháp đặc tả và kiểm chứng thiết kế củachương trình tương tranh để chứng minh tính đúng đắn của thiết kế trước khi cài đặt. Trongcác hệ thống tương tranh, khi có hai hay nhiều luồng cùng truy cập đồng thời và tác động lêntài nguyên dùng chung thì rất dễ xảy ra việc các luồng khác nhau cùng đọc và ghi lên cùngmột phần tử dữ liệu của tài nguyên dùng chung – vấn đề xung đột tài nguyên. Điều này làmcho kết quả của chương trình bị sai và khi xảy ra lỗi kiểu này chúng ta thường khó phát hiệnra vì đây là lỗi ngữ nghĩa. Để tìm ra những lỗi này, chúng ta phải tiến hành phân tích theomột trong hai cách hoặc là đi từ mã nguồn đến thiết kế hoặc ngược lại đi từ thiết kế đến mãnguồn. Như vậy chính việc đảm bảo tính đúng đắn của thiết kế đặc biệt trong các dự án lớnvới một bộ mã nguồn đồ sộ nó sẽ giúp cho chúng ta giảm bớt ...