Khóa luận Kiểm chứng mô hình phần mềm sử dụng nusmv

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Nông Gia Tự KIỂM CHỨNG MÔ HÌNH PHẦN MỀM SỬ DỤNG NUSMV KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ thông tin HÀ NỘI - 2010 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Nông Gia Tự KIỂM CHỨNG MÔ HÌNH PHẦN MỀM SỬ DỤNG NUSMV KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ thông tin Cán bộ hướng dẫn: TS. Phạm Ngọc Hùng HÀ NỘI - 2010 Lời cảm ơn Lời đầu tiên em xin bày tỏ lòng biết ơn sâu sắc tới TS. Phạm Ngọc Hùng, thầy đã hướng dẫn em tận tình trong suốt năm học vừa qua. Em xin bày tỏ lòng biết ơn tới các thầy, cô giáo trong Khoa Công nghệ thông tin - Trường Đại học Công nghệ - ĐHQGHN. Các thầy cô đã dạy bảo, chỉ dẫn chúng em và luôn tạo điều kiện tốt nhất cho chúng em học tập trong suốt quá trình học đại học đặc biệt là trong thời gian làm khoá luận tốt nghiệp. Tôi xin cảm ơn các bạn sinh viên lớp K51CD và lớp K51CNPM đã cho tôi những ý kiến đóng góp giá trị cùng những lời động viên khích lệ khi thực hiện đề tài này. Cuối cùng con xin gửi tới bố mẹ và toàn thể gia đình lòng biết ơn và tình cảm yêu thương. Hà Nội, ngày 15 tháng 5 năm 2008 Nông Gia Tự Tóm tắt Kiểm chứng mô hình (model checking) là một hướng tiếp cận hiệu quả cho việc đảm bảo chất lượng phần mềm. Kĩ thuật này được áp dụng để chứng minh một cách tự động tính đúng đắn của phần mềm hoặc chỉ ra tại sao phần mềm không chạy đúng thông qua phản ví dụ. Hiện nay có rất nhiều công cụ kiểm chứng mô hình phần mềm như NuSMV, SPIN, KRONOS ... Khóa luận này nghiên cứu lý thuyết cơ bản vè kiểm chứng mô hình, ngôn ngữ SMV dùng để mô hình hóa hệ thống và cách sử dụng NuSMV để kiểm chứng mô hình phần mềm. Kiểm chứng mô hình thường được áp dụng ở giai đoạn thiết kế vì việc mô hình hóa bản thiết kế hệ thống dễ dàng hơn mô hình hóa mã nguồn của hệ thống. Ngoài ra, việc sớm tìm ra lỗi ở bản thiết kế sẽ giúp giảm thiểu rủi ro của quá trình phát triển phần mềm. Vì thế chúng tôi tập trung tìm hiểu và đề xuất quy trình kiểm chứng mô hình sử dụng NuSMV ở giai đoạn thiết kế phần mềm. Đồng thời áp dụng quy trình này để kiểm chứng mô hình của phần mềm giả lập máy rút tiền tự động ATM. Mục lục Danh mục hình vẽ Hình 2.1. Nguyên tắc họat động của kiểm chứng mô hình. Hình 2.2. Sơ đồ kiến trúc NuSMV. Hình 5.1. Biểu đồ ca sử dụng hệ thống máy ATM. Hình 5.3. Biểu đồ trạng thái quá trình thực hiện một phiên làm việc của hệ thống ATM. Hình 5.4. Biểu đồ trạng thái quá trình thực hiện giao dịch của hệ thống ATM. Hình 5.5. Mô hình tổng thể hệ thống viết bằng ngôn ngữ SMV. Hình 5.6. Mô hình quá trình thực hiện một phiên làm việc của hệ thống bằng ngôn ngữ SMV. Hình 5.7. Mô hình quá trình thực hiện giao dịch của hệ thống ATM bằng ngôn ngữ SMV. Hình 5.8. Kết quả kiểm chứng mô hình tổng thể hệ thống. Hình 5.9. Kết quả kiểm chứng mô hình phiên làm việc của hệ thống. Hình 5.10. Kết quả kiểm chứng mô hình thực hiện giao dịch hệ thống. Danh mục từ viết tắt Ký hiệu Thuật ngữ ATM Automated Teller Machine BDD Binary Decision Diagram CTL Computation Tree Logic LTL Linear Time Logic Giới thiệu Đặt vấn đề Việc đảm bảo chất lượng phần mềm là một trong những công đoạn khó khăn nhất của việc phát triển phần mềm. Trong đó, việc đảm bảo tính đúng đắn của bản thiết kế ở bước sớm nhất có thể là một thách thức lớn nhất đối với bất kì quy trình phát triển phần mềm nào. Từ trước đến nay, phương pháp giả lập và kiểm thử thường được sử dụng để kiểm tra các bản thiết kế [5]. Tuy nhiên phương pháp này bộc lộ nhiều khiếm khuyết trong đó điểm yếu nghiêm trọng nhất chính là không thể khẳng định được chương trình đã hết lỗi hoặc ước lượng được số lỗi có thể sót lại trong bản thiết kế [5]. Kiểm chứng mô hình là một kỹ thuật kiểm chứng tự động các hệ thống hữu hạn trạng thái. Kiểm chứng mô hình xác minh tính đúng đắn của một mô hình bằng việc xác định xem các thuộc tính người dùng mong muốn có được thỏa mãn bởi mô hình đó hay không [6]. Về nguyên tắc hoạt động, hệ thống cần kiểm chứng sẽ được mô hình hóa. Công cụ kiểm chứng sẽ kiểm tra mô hình có thỏa mãn các thuộc tính được cho hay không. Nhờ khả năng duyệt qua tất cả các trạng thái trong mô hình mà tính đúng đắn của kết quả kiểm chứng mô hình luôn được đảm bảo. Nguyên tắc họat động của kiểm chứng mô hình như sau: Đóng vai trò xử lý dữ liệu tự động là một công cụ kiểm chứng mô hình. Đầu vào là hệ thống cần kiểm chứng đã được mô hình hóa và mô tả các thuộc tính cần kiểm chứng. Đầu ra là kết quả kiểm chứng – kết luận hệ thống hoàn toàn thỏa mãn các thuộc tính hoặc kết luận hệ thống không thỏa mãn một hoặc nhiều thuộc tính đi kèm với phản ví dụ. Nguyên tắc này được minh họa trong hình sau: Hình 2.1. Nguyên tắc họat động của kiểm chứng mô hình [7]. Trong quá trình kiểm chứng mô hình, việc mô hình hóa hệ thống và đặc tả các thuộc tính thường được thực hiện thủ công. Việc chứng minh mô hình có thỏa mãn các thuộc tính hay không đựơc thực hiện tự động bằng công cụ kiểm chứng mô hình. Khóa luận này tập trung nghiên cứu và áp dụng công cụ kiểm chứng mô hình NuSMV vào việc kiểm chứng ở giai đoạn thiết kế phần mềm. Nội dung nghiên cứu của khóa luận NuSMV là một công cụ kiểm chứng mô hình mã nguồn mở. Đầu vào của NuSMV là một file viết bằng ngôn ngữ SMV trong đó mô tả mô hình hệ thống và các đặc tả thuộc tính cần kiểm chứng. Khóa luận nghiên cứu lý thuyết kiểm chứng mô hình và áp dụng NuSMV để kiểm chứng bản thiết kế phần mềm. Quá trình thực hiện bao gồm xác định rõ và đặc tả các thuộc tính cần kiểm chứng, mô hình hóa hệ thống và sử dụng NuSMV để phân tích, chứng minh hệ thống có thỏa mãn các thuộc tính cần kiểm chứng đó hay không. Cấu trúc khóa luận 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 kiến thức cơ bản về kiểm chứng mô hình và giới thiệu về NuSMV, một công cụ kiểm chứng phần mềm. Chương 3 giới thiệu về logic thời gian và sử dụng logic thời gian để mô tả các thuộc tính cần kiểm chứng. Chương 4 trình bày về cú pháp, các kiểu dữ liệu của ngôn ngữ SMV, cách sử dụng ngôn ngữ SMV để mô tả một máy hữu hạn trạng thái. Chương 5 tìm hiểu và đề xuất quy trình kiểm chứng mô hình ở giai đoạn thiết kế phần mềm sử dụng NuSMV, sau đó áp dụng quy trình này vào kiểm chứng mô hình phần mềm giả lập máy rút tiền tự động ATM. Chương 6 nêu ra những kết luận sau khi thực hiện đề tài khóa luận và định hướng khóa luận trong tương lai. Tổng quan về kiểm chứng mô hình và NuSMV Tổng quan về kiểm chứng mô hình Giới thiệu Kiểm chứng mô hình là kỹ thuật phân tích hệ thống để xác định tính hợp lệ của một hay nhiều tính chất mà người dùng quan tâm trong một mô hình cho trước. Cụ thể hơn, với mô hình M và thuộc tính p cho trước, nó kiểm tra liệu thuộc tính p có thỏa mãn trong mô hình M hay không: M |= p [2]. Về mặt thực thi, kiểm chứng mô hình là kỹ thuật tĩnh, nó duyệt qua tất cả các trạng thái, các đường thực thi có thể có trong mô hình M để xác định tính khả thỏa của p. Trên thực tế, mô hình kiểm chứng đã chứng minh rằng nó là một phương thức hiệu quả để phát hiện nhiều lỗi trong các pha thiết kế ban đầu. Kiểm chứng mô hình bao gồm 3 bước: Mô hình hóa, đặc tả và kiểm chứng. Ở bước mô hình hóa, kết quả tạo ra là một mô hình mà các công cụ kiểm chứng có thể sử dụng được. Đầu vào của bước này có thể là bản thiết kế phần mềm hoặc là các dòng mã lập trình. Trong bước tiếp theo, các thuộc tính mà bản thiết kế cần thỏa mãn được đặc tả. Các thuộc tính này thường được diễn đạt bằng các biểu thức logic. Kết quả của hai bước mô hình hóa và đặc tả chính là đầu vào của kiểm chứng mô hình. Ở bước cuối cùng, kiểm chứng, công cụ kiểm chứng sẽ tự động thực hiện và trả về kết quả là thỏa mãn nếu mô hình thỏa mãn các thuộc tính, hoặc đưa ra một phản ví dụ nếu mô hình không thỏa mãn. Dựa vào phản ví dụ, người ta có thể tìm ra được lý do vì sao mô hình không thỏa mãn các thuộc tính đặt ra. Tóm lại, kiểm chứng mô hình là một kĩ thuật giúp kiểm tra một chương trình hoặc một bản thiết kế có thỏa mãn các tính chất đặt ra hay không một cách tự động. Đầu vào của nó là một mô hình cần kiểm chứng và các thuộc tính mà nó cần thỏa mãn. Đầu ra là kết luận mộ hình thỏa mãn các tính chất hoặc đưa ra một phản ví dụ nếu mô hình không thỏa mãn. Ý nghĩa của kiểm chứng mô hình Các hệ thống phần mềm đang ngày càng trở nên cần thiết và đóng vai trò quan trọng trong đời sống hàng ngày. Nhiều công việc có mức độ ảnh hưởng lớn được thực hiện bởi phần mềm như điều khiển đèn giao thông, giao dịch ngân hàng, điều khiển các thiết bị y tế ... Những phần mềm thực hiện các công việc đó phải đảm bảo có độ tin cậy rất cao và không được phép xuất hiện lỗi. Kiểm chứng mô hình cho phép khẳng định được phần mềm hoàn toàn không còn lỗi và thực hiện được đúng các chức năng đã đặt ra. Ngòai ra, kiểm chứng phần mềm còn có ý nghĩa quan trọng trong quy trình phát triển phần mềm. Nó cho phép tìm ra được các lỗi ngay từ giai đoạn thiết kế của quy trình phát triển. Điều này có vai trò rất quan trọng vì các lỗi từ giai đoạn thiết kế nếu tìm ra muộn có thể gây thiệt hại rất lớn so với các lỗi của giai đoạn sau. Sự khác nhau giữa kiểm chứng mô hình phần mềm và kiểm thử phần mềm Cả kiểm chứng mô hình và kiểm thử phần mềm đều thực hiện vai trò đảm bảo chất lượng phần mềm bằng việc tìm ra các lỗi nếu có của phần mềm. Tuy nhiên giữa kiểm chứng mô hình và kiểm thử phần mềm có một số điểm khác nhau quan trọng sau: Kiểm thử phần mềm đòi hỏi phải có chương trình để thực hiện, còn kiểm chứng mô hình thì ngoài kiểm thử trên mã nguồn còn có thể dùng để kiểm chứng bản thiết kế, nghĩa là khi chương trình vẫn còn trên giấy. Kiểm thử phần mềm chỉ có thể khẳng định được chương trình không gặp lỗi đối với các trường hợp kiểm thử đã kiểm tra tức không tìm thấy lỗi chứ không khẳng định được là chương trình hoàn toàn không còn lỗi. Ngược lại, kiểm chứng phần mềm cho phép ta kết luận được chương trình hoàn toàn không còn lỗi. Tuy nhiên, kiểm thử phần mềm có ưu điểm rất lớn là dễ thực hiện. Một người bình thường cũng có thể thực hiện được. Trong khi đó, kiểm chứng mô hình đòi hỏi phải mô hình hóa và đặc tả, công việc này rất khó và đòi hỏi người thực hiện có trình độ kinh nghiệm và kiến thức nhất định. Tóm lại, kiểm chứng mô hình là một phương pháp hiệu quả nhất để kiểm chứng phần mềm. Tuy nhiên để sử dụng được nó một cách hiệu quả đòi hỏi phải mất nhiều thời gian và công sức để nghiên cứu và thực hiện. NuSMV Giới thiệu NuSMV là một công cụ kiểm chứng mô hình được trường đại học Carnegie Mellon University (CMU) và viện per la Ricerca Scientifica e Tecnolgica (IRST). NuSMV được thiết kế với kiến trúc mở, mềm dẻo và được mô tả đầy đủ để phục vụ cho việc kiểm chứng mô hình phần mềm [4]. NuSMV có thể xử lý file viết bằng ngôn ngữ SMV. File này chứa hệ thống đã được mô hình hóa và các đặc tả thuộc tính mà hệ thống cần kiểm chứng. Sau khi xử lý, NuSMV sẽ đưa ra thông báo hệ thống có thỏa mãn các thuộc tính đó hay không, nếu hệ thống không thỏa mãn, NuSMV sẽ đưa ra phản ví dụ. NuSMV hỗ trợ cả đặc tả thuộc tính bằng LTL và CTL. Kiến trúc của NuSMV NuSMV có kiến trúc mở, dễ dàng chỉnh sửa, mở rộng hay nâng cấp. Kiến trúc của NuSMV được chia thành các module. Mỗi module đảm trách một tập hợp các chức năng và giao tiếp với các module khác qua những giao diện đã được định nghĩa rõ ràng. Phần lõi và phần ngoại vi của kiến trúc được tách biệt rõ ràng nhằm giúp cho các module bên trong có thể sử dụng lại một cách độc lập với ngôn ngữ dùng để mô hình hóa hệ thống. Kiến trúc của NuSMV (hình 4.1) bao gồm các module sau: Kernel: Phần lõi. Module này cung cấp các chức năng ở mức độ thấp như cấp phát bộ nhớ động, tổ chức các cấu trúc dữ liệu. Module này có thể được sử dụng lại như những hộp đen (black-box) với những hàm đã được mô tả rõ ràng. Parser: Bộ phân tích ngữ pháp. Module này xử lý file viết bằng ngôn ngữ SMV, kiểm tra về mặt cú pháp và xây dựng cấu trúc cây biểu diễn cấu trúc bên trong của file được xử lý. Compiler: Chương trình dịch. Module này có chức năng dịch file SMV sau khi đã phân tích ngữ pháp sang cây quyết định nhị phân (binary decision diagram - BDD). Mô hình hệ thống được chuyển thành máy hữu hạn trạng thái nhờ module này. Model Checking: Bộ kiểm chứng mô hình. Module này kiểm tra các thuộc tính được mô tả bằng CTL và sinh ra các phản ví dụ nếu thuộc tính không được thỏa mãn bởi mô hình. LTL: Module này có chức năng dịch các biểu thức LTL thành các hoạt cảnh (tableaux) thích hợp để NuSMV có thể xử lý được. Interactive shell: Giao diện tương tác dòng lệnh. Module này cung cấp giao diện người dùng ở chế độ dòng lệnh. Graphical user interface: Giao diện đồ họa người dùng. Module này được xây dựng bên trên module giao diện tương tác dòng lệnh nhằm cung cấp một giao diện đồ họa trực quan của chương trình cho người sử dụng. Hình 2.2. Sơ đồ kiến trúc NuSMV [4]. Sử dụng NuSMV để kiểm chứng mô hình Để kiểm chứng mô hình bằng NuSMV, chúng ta cần mô tả hệ thống và đặc tả các thuộc tính bằng ngôn ngữ SMV. Sau đó sử dụng lệnh: nusmv tên_file trong đó tên_file là tên của file được viết bằng ngôn ngữ SMV. Giới thiệu về logic thời gian Khái niệm Logic thời gian dùng để mô tả các kí hiệu và hệ thống luật về giá trị đúng sai của các vị từ có tính đến yếu tố thời gian. Khác với logic mệnh đề trong đó mỗi mệnh đề có tính chất đúng sai rõ ràng mà không quan tâm đến thời điểm đang xem xét, logic thời gian cho phép biểu diễn các mệnh đề mà giá trị chân lý của nó phụ thuộc vào thời gian. Một ví dụ: Với mệnh đề logic: Trời mưa. Theo logic vị từ, mệnh đề này luôn đúng họăc luôn sai trong bất kì thời điểm nào. Tuy nhiên, giá trị đúng sai của nó có thể thay đổi theo thời gian. Có thể ngày hôm nay trời mưa nhưng ngày mai trời không mưa. Nếu trong logic vị từ, mỗi vị từ chỉ có thể có một giá trị hoặc đúng (bằng 1) hoặc sai (bằng 0) thì trong logic thời gian, mỗi vị từ được coi như một dãy các giá trị mà mỗi phần tử của dãy chỉ có thể có giá trị đúng hoặc sai [9]. Nhờ đó, logic thời gian có thể biểu diễn được sự thay đổi theo thời gian của giá trị các biểu thức logic. Trong các nghiên cứu về kiểm chứng mô hình, hai loại logic thời gian hay được xem xét là LTL và CTL [1]. Các toán tử trong logic thời gian Toán tử globally (toàn thể) Toán tử globally kí hiệu là □. Giả sử ϕ là một biểu thức logic vị từ, khi đó biểu thức □ϕ có giá trị đúng nếu ϕ đúng trong mọi thời điểm. Người ta cũng thường kí hiệu toán tử này là G. Toán tử next (tiếp theo) Toán tử next kí hiệu là ○. Giả sử ϕ là một biểu thức logic. Có thể coi ϕ như một dãy trạng thái và trạng thái hiện tại đang xét đến là trạng thái thứ n. Khi đó biểu thức ○ϕ có giá trị đúng khi và chỉ khi phần tử ngay sau phần tử hiện tại trong dãy trạng thái ϕ (phần tử thứ n+1) có giá trị đúng. (bằng 1) Toán tử next thường được kí hiệu bằng chữ cái X. Toán tử eventually (cuối cùng sẽ xảy ra) Toán tử eventually kí hiệu là ◊. Giả sử ϕ là một biểu thức logic và ϕ được coi như một dãy trạng thái mà mỗi phần tử chỉ có giá trị bằng 0 hoặc 1. Khi đó giá trị biểu thức ◊ϕ bằng 1 khi và chỉ khi ϕ có ít nhất một phần tử có giá trị bằng 1. Toán tử ◊ được định nghĩa thông qua toán tử □ như sau: ◊ϕ ≡ □ φ Toán tử eventually thường được kí hiệu bằng chữ cái F. TLT và CTL Các biểu thức temporal logic không chỉ xét đến những dãy trạng thái đơn, mà còn xét đến những dãy trạng thái phức tạp trong đó từ một trạng thái có thể có nhiều trạng thái ngay tiếp sau nó. Trong các nghiên cứu về kiểm chứng mô hình, hai loại logic thời gian hay được xem xét là LTL và CTL: LTL (linear-time-temporal logic): Logic thời gian tuyến tính. Thời gian có cấu trúc tuyến tính, mỗi trạng thái chỉ có một trạng thái ngay tiếp sau nó. CTL (branching-time-temporal logic): Logic thời gian rẽ nhánh. Thời gian có cấu trúc tuyến tính, mỗi trạng thái có nhiều trạng thái ngay tiếp sau nó. Tóm lại, nhờ khả năng xét đến yếu tố thời gian, temporal logic đã được sử dụng rộng rãi trong công nghệ kiểm chứng phần mềm. Temporal logic thường được sử dụng để mô tả các thuộc tính cần kiểm chứng. Sử dụng temporal logic để mô tả một số thuộc tính cần kiểm chứng Safety (tính an toàn) Tính an toàn của một chương trình đảm bảo rằng sẽ không bao giờ xảy ra tình huống xấu trong chương trình (“something bad never happen”). Tính an toàn có thể được biểu diễn bằng temporal logic như sau: AG ϕ trong CTL hoặc G ϕ trong LTL Trong đó ϕ là một biểu thức logic. Ví dụ của tính an toàn: Nhiệt độ của phản ứng không bao giờ quá 100 độ C. Bất kì lúc nào chìa khóa xe chưa vặn tới vị trí khởi động, xe sẽ không nổ máy. Liveness (tính chạy được) Thuộc tính liveness của một chương trình đảm bảo rằng nó có thể thực thi được một chức năng “tốt” nào đó đã đặt ra. (“something good will happen eventually”). Thuộc tính liveness có thể được biểu diễn bằng các phép kết hợp AF hoặc F trong temporal logic: AF done AG (req → AF grant) AG AF tick trong CTL hoặc F done G (req → F grant) G F tick trong LTL. Ví dụ: Khi chìa khóa xe vặn tới vị trí khởi động, xe sẽ nổ máy. Bóng đèn sẽ chuyển sang màu xanh Fairness (tính công bằng) Tính công bằng đảm bảo rằng nếu một sự kiện nào đó ở trạng thái sẵn sàng được thực thi thì đến một lúc nào đó nó sẽ được thực thi. Thuộc tính công bằng có thể được biểu diễn bằng các toán tử AF và phép suy ra: AG (san_sang=0 → AF thuc_thi=0) AG (san_sang=1→ AF thuc_thi =1) Một ví dụ cho tính công bằng trong một hệ thống truyền-nhận tin là khi một gói tin được gửi đi thì đến một lúc nào đó nó sẽ đến được đích. Ngôn ngữ SMV Tổng quan Ngôn ngữ SMV dùng để mô tả các hệ thống hữu hạn trạng thái. Các kiểu dữ liệu mà ngôn ngữ này cung cấp bao gồm: kiểu logic (boolean), kiểu số nguyên (bounded interger subrange) và các kiểu dữ liệu liệt kê symbolic enum. Các mô tả của một hệ thống phức tạp có thể được chia nhỏ thành các module và mỗi một module này có thể được thực thi nhiều lần. Cấu trúc của chương trình viết bằng ngôn ngữ SMV Một chương trình viết bằng ngôn ngữ SMV có các phần như sau: MODULE tên_module VAR Khai báo các biến. ASSIGN Mô tả các bước chuyển trạng thái của hệ thống. Kết thúc câu lệnh là một dấu chấm phẩy (;). Các kiểu dữ liệu Khai báo kiểu dữ liệu Các mô tả của một hệ thống phức tạp có thể được chia nhỏ thành các module và mỗi một module này có thể được thực thi nhiều lần. Một biểu thức khai báo biến có định dạng như sau: : ; Trong đó là tên của biến cần khai báo, còn là kiểu dữ liệu của biến đó. Ví dụ, khai báo biến request với kiểu dữ liệu là boolean như sau: request : boolean; Kiểu logic (boolean), kiểu số nguyên (integer) và kiểu liệt kê (enum) Kiểu logic chỉ chứa giá trị 0 hoặc 1. Ví dụ khi khai báo một biến logic: var1:boolean thì biến var1 chỉ có thể có giá trị bằng 1 hoặc 0. Kiểu liệt kê là một tập hợp các giá trị. Ví dụ, câu lệnh var1: {ready, willing, able}; khai báo một biến có thể có các giá trị là ‘ready’, ‘willing’, ‘able’. Ngoài ra, các giá trị của một kiểu biến liệt kê có thể là các số nguyên. Ví dụ như câu lệnh sau khai báo một biến có tên là count có thể có các giá trị là những số nguyên từ 0 đến 7: count: 0..7; Các giá trị số trong khai báo biến cũng có thể là các biểu thức chứa các chữ số và các toán tử như +, - , *, /, mod, > và **. Mảng Một mảng trong ngôn ngữ SMV được khai báo theo dạng sau: : array .. of Câu lệnh trên sẽ khai báo một mảng các phần tử có kiểu là , chỉ số của phần tử chạy từ đến . Ví dụ, câu lệnh: var1 : array 2..0 of boolean; tương đương với khai báo như sau: var1[2] : boolean; var1[1] : boolean; var1[0] : boolean; Một phần tử của mảng có thể được tham chiếu nhờ chỉ số của nó nằm trong dấu ngoặc vuông viết sau tên biến. Nhưng chỉ số này cần phải nằm trong khoảng đã khai báo. Mảng nhiều chiều Một mảng trong ngôn ngữ SMV được khai báo theo dạng sau: Một mảng hai chiều có thể được coi như một mảng của mảng. Ví dụ, câu lệnh: matrix : array 0..1 of array 2..0 of boolean; Tương đương với khai báo sau: matrix[0] : array [2..0] of boolean; matrix[1] : array [2..0] of boolean; Kết quả, ta đã định nghĩa một ma trận với 2 hàng và 3 cột như sau: matrix[0][0] matrix[0][1] matrix[0][2] matrix[1][0] matrix[1][1] matrix[1][2] Số chiều của mảng là không giới hạn. Chú ý rằng một mảng trong ngôn ngữ SMV không hoàn toàn là một kiểu dữ liệu. Nó đơn giản chỉ là một tập hợp các biến đơn lẻ. Điều đó có nghĩa là hoàn toàn có thể định nghĩa một mảng chứa các phần tử có kiểu dữ liệu khác nhau, bằng cách khai báo giá trị của từng phần tử trong mảng. Ví dụ: state[0] : {ready, willing}; state[1] : {ready, willing, able}; state[2] : {ready, willing, able, exhausted}; Kiểu cấu trúc Kiểu cấu trúc của SMV cũng giống như của các ngôn ngữ lập trình như C, Java ... Nó là một tập hợp các giá trị. Một biến có kiểu cấu trúc có thể được khai báo như sau: foo : struct { c1 : kiểu_1; c2 : kiểu_2; ... cn : kiểu_n; } Trong đó c1, c2 ... cn là các tên biến. Khai báo trên tương đương với khai báo sau: foo.c1 : kiểu_1; foo.c2 : kiểu_2; .. foo.cn : kiểu_n; Như vậy, kiểu cấu trúc cũng giống như kiểu mảng ở điểm có thể chứa nhiều phần tử với những kiểu dữ liệu khác nhau Biến và các phép gán Giá trị của một biến là một chuỗi các giá trị. Chuỗi này không giới hạn về độ dài và các giá trị của chuỗi phải thuộc kiểu dữ liệu của biến đó. Ví dụ, một biến kiểu logic có thể có giá trị bằng: 0;1;0;1; Các phép toán Như ta đã biết, giá trị của một biến có thể là một chuỗi các phần tử. Một phép toán tác động đến từng phần tử đó. Ví dụ, xét trường hợp phép toán NOT, ký hiệu là “~”, áp dụng cho biến sau: foo = 0;1;0;1;... ta được kết quả ~foo = 1;0;1;0;... Một phép toán khác là phép toán AND, ký hiệu là “&”. Ví dụ: foo = 0;1;0;1;... và bar = 0;0;1;1;... khi đó foo & bar = 0;0;0;1;... Phép gán Như ta đã biết, giá trị của một biến có thể là một chuỗi các phần tử. Một phép toán tác động đến từng phần tử đó. Ví dụ, xét trường hợp phép toán NOT, ký hiệu là “~”, áp dụng cho biến sau: Phép gán là một biểu thức có dạng: := ; Trong đó là một biểu thức kết hợp các biến và các phép toán như “~” và “&”. Sau khi thực hiện câu lệnh trên, biến ở vế trái sẽ có giá trị bằng giá trị của biểu thức ở vế phải. Ví dụ, với phép gán: zip := foo & bar với các giá trị của biến foo và bar ở trên ta được zip := 0;0;0;1;... Các phép gán trong ngôn ngữ SMV được thông dịch đồng thời. Như vậy thật ra hai phép gán liên tiếp nhau trong một chương trình không có nghĩa là chúng được thực hiện tuần tự. Ví dụ với hai phép gán trong một chương trình: y := x + 1; z := y + 1; chúng ta có z := x + 2; Tóan tử next Các phép gán trong ngôn ngữ SMV được thông dịch đồng thời. Như vậy thật ra hai phép gán liên tiếp nhau trong một chương trình không có nghĩa là chúng được thực hiện tuần tự. Ví dụ với hai phép gán trong một chương trình: Giả sử với x là một biến, khi đó next(x) sẽ là giá trị tiếp theo của x. Nói cách khác, giá trị thứ i của next(x) bằng giá trị thứ (i+1) của biến x. Ví dụ: x = 0, 1, 2, 3 ... thì next(x) = 1, 2, 3, 4 ... Bằng cách gán giá trị cho giá trị “next” của một biến, chúng ta có thể định nghĩa được một máy tuần tự. Ví dụ với x và y là hai biến kiểu logic, câu lệnh next(x) := y ^ x; định nghĩa một biến x mà sẽ đảo ngược mỗi khi biến y bằng 1. Theo định nghĩa, (y^x) sẽ trả về giá trị bằng x nếu y sai và bằng ~x nếu y đúng. Tuy nhiên, vì chưa khai báo giá trị khởi đầu của biến x nên chúng ta sẽ thu được những dãy khác nhau tùy thuộc vào biến x khởi đầu là 1 hay là 0. Chúng ta có thể khai báo giá trị khởi đầu của biến x bằng câu lệnh như sau: init(x) := 0; Với giá trị khởi đầu này, giả sử với y = 0; 1; 0; 1 ... ta được x = 0; 0; 1; 1; 0 ... Mặt khác, nếu ta khai báo init(x) := 1; Ta được x = 1; 1; 0; 0; 1 ... Máy trạng thái Chúng ta có thể khai báo giá trị khởi đầu của biến x bằng câu lệnh như sau: Một ví dụ về máy hữu hạn trạng thái: Trạng thái bắt đầu là “idle” và chờ đến khi xuất hiện tín hiệu “start”. Trong chu kì tiếp theo, nó chuyển sang trạng thái “cyc1”, tiếp đến là “cyc2”, rồi trở lại trạng thái “idle”. Ở trạng thái “cyc2”, nó tạo ra tín hiệu “done”. start,done : boolean; state : {idle,cyc1,cyc2}; next(state) := switch(state){ idle: start ? cyc1 : idle; cyc1: cyc2; cyc2: idle; }; done := (state = cyc2); Đoạn mã trên có sử dụng hai dạng câu lệnh rẽ nhánh. Toán tử switch cũng giống trong các ngôn ngữ lập trình như C hay Java. Trong trường hợp này nó nhận đối số đầu vào là giá trị của biến state và nhảy đến nhánh có gán nhãn là giá trị này. Ví dụ, ban đầu biến state có giá trị là idle, câu lệnh switch(state) sẽ nhảy đến câu lệnh vế phải của nhãn idle. Một câu lệnh rẽ nhánh khác sử dụng toán tử “?”. Toán tử này cũng tương tự trong ngôn ngữ lập trình C. Ví dụ với câu lệnh: Start ? cyc1 : idle Nếu start là đúng thì trả về giá trị cyc1, ngược lại trả về idle. Ngoài ra ngôn ngữ SMV cũng có toán tử if, then dùng để rẽ nhánh tương tự như trong ngôn ngữ Pascal. Đoạn mã lệnh sau cũng tương tự đoạn mã lệnh phía trên: default done := 0; in switch(state){ idle: if start then next(state) := cyc1; cyc1: next(state) := cyc2; cyc2: next(state) := cyc2; done := 1; } Tuy đoạn mã này có chức năng giống hệt đoạn mã trước nhưng có cấu trúc rõ ràng và dễ đọc hơn. Tóm lại, ngôn ngữ SMV là một ngôn ngữ mô tả một máy trạng thái hữu hạn trong đó không có những phụ thuộc vòng và chuyển trạng thái nhập nhằng. Ngôn ngữ SMV có thể dùng để thiết lập mô hình dùng cho việc kiểm chứng. Áp dụng NuSMV kiểm chứng mô hình phần mềm giả lập máy ATM Đề xuất quy trình đặc tả và kiểm chứng phần mềm sử dụng NuSMV Những cơ sở để đưa ra quy trình Để kiểm chứng một mô hình cần phải thực hiện hai bước: đầu tiên phải mô hình hóa phần mềm cần kiểm chứng sau đó cần định nghĩa các thuộc tính cần kiểm chứng. Đối với trường hợp sử dụng NuSMV thì chúng ta cần hai bước là mô hình hóa bằng ngôn ngữ SMV và khai báo các thuộc tính cần kiểm chứng bằng temporal logic. Việc xây dựng mô hình có ý nghĩa vô cùng quan trọng. Nếu mô hình được xây dựng không chính xác, nó sẽ không mô tả đúng hệ thống cần kiểm chứng. Khi đó, kết quả kiểm chứng sẽ không còn chính xác nữa. Ngoài ra, do việc xây dựng mô hình bằng ngôn ngữ SMV được thực hiện thủ công nên có thể xảy ra sai sót. Quy trình sau được đưa ra với mục đích làm cho việc mô hình hóa trở nên dễ dàng và đảm bảo độ chính xác cao. Bản chất của ngôn ngữ SMV là một ngôn ngữ mô tả một máy hữu hạn trạng thái. Do đó một máy hữu hạn trạng thái và không có các chuyển trạng thái lặp vô hạn thì sẽ ánh xạ tương ứng một mô hình bằng ngôn ngữ SMV. Dựa vào tính chất này, chúng ta sẽ tìm cách xây dựng các biểu đồ trạng thái của hệ thống cần kiểm chứng rồi từ biểu đồ trạng thái xây dựng mô hình bằng ngôn ngữ SMV. Mô tả quy trình Mục tiêu của quy trình này là kiểm chứng phần mềm ở giai đoạn thiết kế hệ thống. Việc kiểm chứng được thực hiện sau khi đã xây dựng được các biểu đồ trạng thái của hệ thống cần xây dựng. Đối tượng của kiểm chứng chính là mô hình hoạt động dự kiến của phần mềm. Sau đây là diễn giải quy trình một cách chi tiết: Bước 1: Xây dựng các đặc tả của hệ thống như thường lệ. Ở bước này cần xác định rõ những thuộc tính cần kiểm chứng mà hệ thống đòi hỏi. Các thuộc tính này sẽ được sử dụng để biểu diễn bằng temporal logic trong bước 3. Bước 2: Thiết kế hệ thống. Bước này được thực hiện như thường lệ. Mục tiêu của bước này là xây dựng được các biểu đồ trạng thái mô tả hoạt động của hệ thống cần xây dựng. Bước 3: Từ biểu đồ trạng thái chúng ta xây dựng mô hình bằng ngôn ngữ SMV. Các thuộc tính cần kiểm chứng đã được xác định trong bước 1 được đặc tả bằng temporal logic. Đưa các đặc tả thuộc tính này vào file mô hình hóa bằng ngôn ngữ SMV. Bước 4: Sử dụng NuSMV để kiểm chứng mô hình có thỏa mãn các thuộc tính đã đặc tả hay không. Đặc tả và kiểm chứng mô hình phần mềm giả lập máy ATM Đặc tả yêu cầu Mô tả bài toán Mục tiêu của quy trình này là kiểm chứng phần mềm ở giai đoạn thiết kế hệ thống. Việc kiểm chứng được thực hiện sau khi đã xây dựng được các biểu đồ trạng thái của hệ thống cần xây dựng. Đối tượng của kiểm chứng chính là mô hình hoạt động dự kiến của phần mềm. Để đơn giản và dễ hiểu cho việc minh họa phương pháp trên, chúng ta xét bài toán: Thiết kế một chương trình phần mềm mô phỏng sự hoạt động của máy ATM. Phần mềm này sẽ mô phỏng một máy ATM. Máy ATM này có một đầu đọc thẻ, một màn hình hiển thị, một khe để xuất tiền, một máy in để in hóa đơn, một công tắc để tắt và bật toàn bộ máy ATM. Máy ATM sẽ giao tiếp với máy chủ của ngân hàng qua mạng. Tuy nhiên phần giao tiếp với ngân hàng không đựơc xét đến trong ví dụ này. Mỗi lần sử dụng, khách hàng sẽ phải đưa thẻ ATM vào và nhập mã PIN. Dữ liệu sẽ được kiểm tra. Sau đó khách hàng có thể thực hiện một hoặc nhiều giao dịch. Thẻ ATM sẽ vẫn ở trong máy cho đến khi người dùng không muốn thực hiện thêm bất kì giao dịch nào nữa và chọn lấy lại thẻ, ngoại trừ trường hợp sẽ nói đến sau đây. Máy ATM sẽ cung cấp cho khách hàng những dịch vụ sau: Khách hàng có thể rút tiền từ tài khoản. Khách hàng có thể chuyển khoản. Khách hàng có thể xem số dư tài khoản. Sau khi khách hàng chọn việc thực hiện một giao dịch, máy ATM sẽ chuyển các dữ liệu về ngân hàng để kiểm tra. Nếu mã PIN của khách hàng không hợp lệ với giao dịch đó, máy ATM sẽ yêu cầu khách hàng nhập lại mã PIN. Nếu khách hàng nhập sai mã PIN ba lần, máy ATM sẽ giữ thẻ ATM và người dùng phải liên hệ với ngân hàng để lấy lại thẻ. Nếu giao dịch không được thực hiện thành công, máy ATM sẽ hiển thị một thông báo lỗi. Sau mỗi giao dịch, máy ATM sẽ hiển thị thông báo hỏi người dùng có muốn thực hiện giao dịch khác hay không. Máy ATM cũng có một công tắc khởi động để bật và tắt toàn bộ máy. Các tác nhân của hệ thống Hệ thống có ba tác nhân sau: Người điều hành: Người thực hiện các chức năng bật máy, tắt máy để bảo trì hệ thống. Người dùng: Người sử dụng hệ thống để thực hiện các giao dịch. Ngân hàng: Có vai trò kiểm tra thông tin và phê duyệt các giao dịch được hệ thống yêu cầu. Mô hình ca sử dụng tổng thể hệ thống Nếu giao dịch không được thực hiện thành công, máy ATM sẽ hiển thị một thông báo lỗi. Người điều hành có thể bật máy hoặc tắt máy ATM để bảo trì. Trong một thời điểm, máy ATM chỉ thực hiện được một phiên làm việc để phục vụ người dùng. Phiên làm việc bao gồm nhiều giao dịch, tại đó người dùng có thể thực hiện việc chuyển tiền, rút tiền, vấn tin tài khoản. Trong mỗi giao dịch, máy ATM sẽ gửi yêu cầu giao dịch đến ngân hàng. Ngân hàng sẽ xác minh lại thông tin và quyết định phê duyệt giao dịch đó hay không. Nếu trong lúc giao dịch, người dùng nhập sai mã PIN nhiều lần thì máy ATM sẽ ngừng giao dịch đó lại và giữ lại thẻ của người dùng. Các ca sử dụng này được mô tả như trong hình sau: Người điều hành Người dùng Ngân hàng Bật máy Tắt máy Phiên làm việc Giao dịch Rút tiền Chuyển tiền Vấn tin tài khoản Sai mã PIN > > Biểu đồ ca sử dụng hệ thống máy ATM. Bật máy Người bảo trì hệ thống ATM bật máy lên để máy ATM có thể làm việc và phục vụ khách hàng. Tắt máy Người bảo trì hệ thống tắt máy ATM, máy ATM ở trạng thái ngưng họat động cho đến khi nào được bật lên. Phiên làm việc Máy ATM vào phiên làm việc. Một phiên làm việc bắt đầu khi khách hàng đưa thẻ ATM vào khe đọc thẻ. Máy ATM đưa thẻ vào trong và đọc thẻ (nếu bộ đọc thẻ không đọc được thẻ thì máy sẽ đưa thẻ ra). Hệ thống sẽ yêu cầu khách hàng nhập mã PIN, sau đó hệ thống sẽ đưa ra một danh sách các loại giao dịch để khách hàng lựa chọn. Sau khi một giao dịch đựơc thực hiện, hệ thống sẽ hỏi khách hàng có muốn thực hiện giao dịch nào khác hay không. Nếu khách hàng chọn không thực hiện giao dịch nào nữa thì máy ATM trả lại thẻ cho khách hàng. Nếu một giao dịch bị dừng do quá nhiều lần nhập sai mã PIN thì phiên giao dịch kết thúc và thẻ ATM của khách hàng bị giữ lại trong máy. Khách hàng có thể kết thúc một phiên làm việc bằng cách ấn nút Cancel trong khi đang nhập mã PIN họăc chọn một loại giao dịch Giao dịch rút tiền Rút tiền. Hệ thống sẽ yêu cầu người dùng chọn tài khoản muốn rút. Sau đó yêu cầu người dùng chọn số tiền từ danh sách các số tiền có thể rút. Hệ thống sẽ kiểm tra xem hiện có đủ tiền để thực hiện giao dịch hay không. Nếu đủ, hệ thống sẽ gửi một yêu cầu phê duyệt tới ngân hàng, nếu không đủ, hệ thống sẽ yêu cầu người dùng chọn số tiền khác. Sau khi yêu cầu rút tiền được ngân hàng phê duyệt, số tiền tương ứng sẽ được đưa ra khỏi máy ATM cho người dùng và sau đó một hóa đơn được xuất ra. Giao dịch rút tiền có thể được dừng lại và bỏ qua nếu người dùng ấn nút Cancel bất kì khi nào số tiền cần rút chưa được chọn. Giao dịch chuyển tiền Hệ thống sẽ yêu cầu người dùng chọn chuyển tiền từ tài khoản nào trong danh sách tài khoản. Sau đó yêu cầu người dùng chọn một tài khoản để chuyển tiền tới. Tiếp theo hệ thống yêu cầu nhập số tiền muốn chuyển. Sau đó hệ thống gửi yêu cầu phê duyệt đến ngân hàng. Nếu yêu cầu chuyển tiền hợp lệ và được ngân hàng phê duyệt, hệ thống sẽ thông báo giao dịch thành công. Giao dịch vấn tin tài khoản Hệ thống hiển thị ra một danh sách các tài khoản và yêu cầu người dùng chọn tài khoản cần vấn tin. Sau khi yêu cầu vấn tin được phê duyệt bởi ngân hàng, hệ thống hiển thị thông báo và in thông tin tài khỏan cho người dùng. Sai mã PIN Trường hợp này xảy ra trong khi thực hiện giao dịch, ngân hàng kiểm tra thông tin và xác định mã PIN không đúng. Hệ thống sẽ dừng giao dịch hiện hành và yêu cầu người dùng nhập lại mã PIN. Nếu mã PIN nhập lại đúng, giao dịch bị dừng sẽ được tiếp tục thực hiện. Nếu mã PIN được nhập sai 3 lần thì hệ thống sẽ giữ lại thẻ ATM của khách hàng và chấm dứt phiên làm việc. Đặc tả các thuộc tính cần kiểm chứng Về tổng thể hệ thống, chúng ta cần đảm bảo rằng hệ thống từ trạng thái đang ngừng họat động đến một lúc nào đó có thể đến trạng thái phục vụ người dùng (liveness). Trong quá trình thực hiện một phiên làm việc, chúng ta muốn đảm bảo rằng, sau khi đưa thẻ vào, cuối cùng nó phải được trả lại người dùng hoặc giữ lại trong thẻ ATM. Trong mỗi giao dịch, yêu cầu thực hiện giao dịch cần được gửi đến ngân hàng để phê duyệt. Do đó chúng ta cần đảm bảo rằng, không có giao dịch nào được thực hiện hoàn tất nếu trước đó nó chưa được gửi đến ngân hàng để phê duyệt. Thiết kế hệ thống Ở bước này, hệ thống được thiết kế. Sản phẩm của bước này là các biểu đồ tương tác, biểu đồ trạng thái, biểu đồ lớp ... Tuy nhiên, do trong quy trình kiểm chứng phần mềm chúng ta xây dựng mô hình dựa trên biểu đồ trạng thái nên ở đây, để cho ngắn gọn, chúng ta chỉ xét đến một số biểu đồ trạng thái nhằm minh họa cho việc thực hiện quy trình. Biểu đồ trạng thái tổng thể hệ thống Sau đây là biểu đồ trạng thái tổng thể hệ thống (bao gồm ca sử dụng bật máy và tắt máy) Biểu đồ trạng thái tổng thể hệ thống ATM. Biểu đồ trạng thái quá trình thực hiện một phiên làm việc của hệ thống Sau đây là biểu đồ trạng thái quá trình thực hiện một phiên làm việc của hệ thống: Đọc thẻ Đọc mã PIN Chọn giao dịch Thực hiện giao dịch Đưa thẻ ra Dừng vì mã PIN nhập sai nhiều lần Chọn giao dịch khác Người dùng chọn “Kết thúc” Giao dịch được chọn Đọc mã PIN thành công Đọc thẻ thành công Thẻ không đọc được/ Hiển thị thông báo “Thẻ không hợp lệ” Nhấn nút Cancel Nhấn nút Cancel Biểu đồ trạng thái quá trình thực hiện một phiên làm việc của hệ thống ATM. Biểu đồ trạng thái quá trình thực hiện giao dịch của hệ thống Sau đây là biểu đồ trạng quá trính thực hiện một giao dịch của hệ thống: Lấy thông tin Gửi thông tin đến ngân hàng Xử lý trường hợp sai mã PIN Hòan thành giao dịch In hóa đơn Hỏi người dùng có thực hiện giao dịch khác không Bỏ qua Thông tin được nhập vào Mã PIN không đúng Ngân hàng phê duyệt Mã PIN được phê duyệt Bỏ qua in hóa đơn Chọn in hóa đơn Bỏ qua Nhập sai mã PIN nhiều lần Ngân hàng không phê duyệt Biểu đồ trạng thái quá trình thực hiện giao dịch của hệ thống ATM. Mô hình hóa hệ thống bằng ngôn ngữ SMV Mô hình hóa tổng thể hệ thống Dựa vào biểu đồ trạng thái tổng thể hệ thống, chúng ta xây dựng được mô hình bằng ngôn ngữ SMV như sau: MODULE main VAR state_overall: {TAT, CHO, PHUC_VU}; VAR action: {BAT_MAY, TAT_MAY, KHOI_TAO_PHIEN_LAM_VIEC, PHIEN_LAM_VIEC_HOAN_TAT, PHIEN_LAM_VIEC_BI_NGUNG}; ASSIGN init(state_overall) := TAT; init(action) := BAT_MAY; next(state_overall) := case (state_overall = TAT) & (action = BAT_MAY): CHO; (state_overall = CHO) & (action = TAT_MAY): TAT; (state_overall = CHO) & (action = KHOI_TAO_PHIEN_LAM_VIEC): PHUC_VU; (state_overall = PHUC_VU) & (action = PHIEN_LAM_VIEC_HOAN_TAT): CHO; (state_overall = PHUC_VU) & (action = PHIEN_LAM_VIEC_BI_NGUNG): CHO; 1: state_overall; esac; Mô hình tổng thể hệ thống viết bằng ngôn ngữ SMV. Trong mô hình này, chúng ta cần đảm bảo rằng hệ thống từ trạng thái đang ngừng họat động đến một lúc nào đó có thể đến trạng thái phục vụ người dùng (liveness). Thuộc tính này được mô tả bằng CTL trong ngôn ngữ SMV như sau: SPEC AG((state_overall = TAT) -> EF(state_overall = PHUC_VU)) Mô hình hóa quá trình thực hiện phiên làm việc Dựa vào biểu đồ trạng thái quá trình thực hiện phiên làm việc của hệ thống (hình 5.3), chúng ta xây dựng được mô hình bằng ngôn ngữ SMV như sau: MODULE main VAR state_session: {DOC_THE, -- doc the DOC_MA_PIN, -- doc ma PIN CHON_GIAO_DICH, -- chosing transaction THUC_HIEN_GIAO_DICH, -- performing transaction TRA_LAI_THE, -- ejecting card KET_THUC}; -- KET_THUC session and not reject card VAR action_session: {THE_KHONG_DOC_DUOC, -- the khong doc duoc DOC_THE_THANH_CONG, -- doc the thanh cong NHAN_NUT_BO_QUA, -- nhan nut bo qua DOC_MA_PIN_THANH_CONG, -- doc ma PIN thanh cong GIAO_DICH_DUOC_CHON, -- giao dich duoc chon KHACH_HANG_CHON_THUC_HIEN_GIAO_DICH_KHAC, -- khach hang chon thuc hien giao dich khac KHACH_HANG_CHON_KET_THUC, -- khach hang chon ket thuc phien lam viec NGUNG_VI_NHAP_MA_PIN_SAI_QUA_NHIEU}; -- ngung giao dich vi nhap ma PIN sai qua nhieu ASSIGN init(state_session) := DOC_THE; next(state_session) := case -- reading card (state_session = DOC_THE) & (action_session = THE_KHONG_DOC_DUOC): TRA_LAI_THE; (state_session = DOC_THE) & (action_session = DOC_THE_THANH_CONG): DOC_MA_PIN; -- reading pin (state_session = DOC_MA_PIN) & (action_session = NHAN_NUT_BO_QUA): TRA_LAI_THE; (state_session = DOC_MA_PIN) & (action_session = DOC_MA_PIN_THANH_CONG): CHON_GIAO_DICH; -- choosing transaction (state_session = CHON_GIAO_DICH) & (action_session = NHAN_NUT_BO_QUA): TRA_LAI_THE; (state_session = CHON_GIAO_DICH) & (action_session = GIAO_DICH_DUOC_CHON): THUC_HIEN_GIAO_DICH; -- performing transaction (state_session = THUC_HIEN_GIAO_DICH) & (action_session = KHACH_HANG_CHON_THUC_HIEN_GIAO_DICH_KHAC): CHON_GIAO_DICH; (state_session = THUC_HIEN_GIAO_DICH) & (action_session = KHACH_HANG_CHON_KET_THUC): TRA_LAI_THE; (state_session = THUC_HIEN_GIAO_DICH) & (action_session = NGUNG_VI_NHAP_MA_PIN_SAI_QUA_NHIEU): KET_THUC; -- ejecting card (state_session = TRA_LAI_THE) : KET_THUC; 1: state_session; esac; Mô hình quá trình thực hiện một phiên làm việc của hệ thống bằng ngôn ngữ SMV. Trong mô hình này, chúng ta muốn đảm bảo rằng, sau khi đưa thẻ vào, cuối cùng nó phải được trả lại người dùng hoặc giữ lại trong thẻ ATM (tức là hệ thống phải đạt đến trạng thái END): SPEC AG ((state_session = DOC_THE) -> EF(state_session = KET_THUC)) Mô hình hóa quá trình thực hiện giao dịch Dựa vào biểu đồ trạng thái quá trình thực hiện giao dịch của hệ thống (hình 5.4), chúng ta xây dựng được mô hình bằng ngôn ngữ SMV như sau: MODULE main VAR state_transaction: {LAY_THONG_TIN, -- lay thong tin GUI_THONG_TIN_DEN_NGAN_HANG, -- gui thong tin den ngan hang XU_LY_SAI_MA_PIN, -- chosing transaction HOAN_THANH_GIAO_DICH, -- hoan thanh giao dich THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG, -- thuc hien giao dich khac hay khong IN_HOA_DON, -- in hoa don KET_THUC}; -- ket thuc VAR action_session: { BO_QUA, -- an nut bo qua THONG_TIN_DUOC_NHAP_VAO, -- thong tin duoc nhap vao hop le NGAN_HANG_KHONG_PHE_DUYET, -- ngan hang khong phe duyet NGAN_HANG_PHE_DUYET, -- ngan hang phe duyet MA_PIN_KHONG_DUNG, -- ma PIN khong dung NHAP_SAI_MA_PIN_NHIEU_LAN, -- nhap sai ma PIN nhieu lan MA_PIN_DUOC_PHE_DUYET, -- ma PIN duoc phe duyet CHON_IN_HOA_DON, -- chon in hoa don BO_QUA_IN_HOA_DON}; -- bo qua in hoa don ASSIGN init(state_transaction) := LAY_THONG_TIN; next(state_transaction) := case -- lay thong tin (state_transaction = LAY_THONG_TIN) & (action_session = BO_QUA): THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG; (state_transaction = LAY_THONG_TIN) & (action_session = THONG_TIN_DUOC_NHAP_VAO): GUI_THONG_TIN_DEN_NGAN_HANG; -- gui thong tin den ngan hang (state_transaction = GUI_THONG_TIN_DEN_NGAN_HANG) & (action_session = NGAN_HANG_KHONG_PHE_DUYET): THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG; (state_transaction = GUI_THONG_TIN_DEN_NGAN_HANG) & (action_session = NGAN_HANG_PHE_DUYET): HOAN_THANH_GIAO_DICH; (state_transaction = GUI_THONG_TIN_DEN_NGAN_HANG) & (action_session = MA_PIN_KHONG_DUNG): XU_LY_SAI_MA_PIN; -- xu ly sai ma PIN (state_transaction = XU_LY_SAI_MA_PIN) & (action_session = NHAP_SAI_MA_PIN_NHIEU_LAN): KET_THUC; (state_transaction = XU_LY_SAI_MA_PIN) & (action_session = BO_QUA): THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG; (state_transaction = XU_LY_SAI_MA_PIN) & (action_session = MA_PIN_DUOC_PHE_DUYET): HOAN_THANH_GIAO_DICH; -- hoan thanh giao dich (state_transaction = HOAN_THANH_GIAO_DICH) & (action_session = CHON_IN_HOA_DON): IN_HOA_DON; (state_transaction = HOAN_THANH_GIAO_DICH) & (action_session = BO_QUA_IN_HOA_DON): THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG; -- in hoa don (state_transaction = IN_HOA_DON) : THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG; -- hoi nguoi dung co thuc hien giao dich khac hay khong (state_transaction = THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG) : KET_THUC; 1: state_transaction; esac; Mô hình quá trình thực hiện giao dịch của hệ thống ATM bằng ngôn ngữ SMV. Trong mô hình này, chúng ta muốn đảm bảo rằng không có giao dịch nào được thực hiện mà trước đó dữ liệu không được gửi đến ngân hàng để phê duyệt: !AG (!(state_transaction = GUI_THONG_TIN_DEN_NGAN_HANG) -> EF(state_transaction = HOAN_THANH_GIAO_DICH)) Kiểm chứng mô hình Kết quả kiểm chứng cho thấy mô hình được thiết kế hoàn toàn thỏa mãn các thuộc tính đặt ra: Kết quả kiểm chứng mô hình tổng thể hệ thống. Kết quả kiểm chứng mô hình phiên làm việc của hệ thống. Kết quả kiểm chứng mô hình thực hiện giao dịch hệ thống. Kết luận Trong khóa luận này chúng tôi đã trình bày những lý thuyết cơ bản về kiểm chứng mô hình phần mềm, nghiên cứu và áp dụng kỹ thuật kiểm chứng mô hình sử dụng NuSMV như là một công cụ kiểm chứng. Chúng tôi đã đề xuất quy trình kiểm chứng mô hình phần mềm ở giai đoạn thiết kế hệ thống sử dụng NuSMV. Quy trình này được áp dụng vào kiểm chứng mô hình phần mềm giả lập máy rút tiền tự động ATM và đã chứng minh được bản thiết kế hoàn toàn thỏa mãn các thuộc tính đặt ra. Khóa luận đã áp dụng thành công kỹ thuật kiểm chứng mô hình vào kiểm chứng ở giai đoạn thiết kế phần mềm. Tuy nhiên, chúng tôi chưa xét đến việc thẩm định lại bản thiết kế hệ thống nếu công cụ kiểm chứng trả về kết quả mô hình hệ thống không thỏa mãn các thuộc tính. Khi đó có thể do bản thiết kế hệ thống sai hoặc bị mô hình hóa sai. Hướng phát triển tiếp theo của đề tài này có thể là áp dụng NuSMV để kiểm chứng mã nguồn phần mềm. Một hướng khác là xây dựng công cụ mô hình hóa tự động bản thiết kế phần mềm. Tài liệu tham khảo B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A Petit, L. Petrucci, P. Schnoebelen. Systems and Software Verification: model-checking techniques and tools, 2001. R. C. Bjork. An Example of Object-Oriented Design: An ATM Simulation. M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: A Model-Checking Tool for Real-Time Systems. Proceedings of the 10th international Conference on Computer Aided Verification (June 28 - July 02, 1998). A. J. Hu and M. Y. Vardi, Eds. Lecture Notes In Computer Science, vol. 1427. Springer-Verlag, London, 546-550. A. Cimatti, E. Clarke, F. Giunchiglia, M. Roveri. NuSMV: a new symbolic model checker. A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In Proceedings of the 14th international Conference on Computer Aided Verification (July 27 - 31, 2002). E. M. Clarke, Orna Grumberg and Doron A. Peled. Model Checking. MIT Press, 1999, ISBN 0-262-03270-8. H. Giese, Safety – Critical computer systems, AG Softwaretechnik, SCCS-VI-6x, 2003. G. J. Holzmann. The Model Checker SPIN. IEEE Trans. Softw. Eng. 23, 5 (May. 1997), 279-295. Kröger, Fred, Merz, Stephan, Temporal logic and state systems, Springer, 2008. ISBN: 978-3-540-67401-6. M. Mansouri-Samani, S. Pasareanu, J. Penix, C. Mehlitz, O. Malley, C. Visser, P. Brat, Z. Markosian and T. Pressburger. Program model checking: A practitioner’s guide, Intelligent Systems Division NASA Ames Research Center. April 27, 2007, pages. 31 – 45.