Mở đầu 8 Theo cách tiếp cận kiểm chứng tại thời điểm thực thi, luận án đề xuất hai phương pháp sử dụng lập trình hướng khía cạnh với AOP để kiểm chứng sự tuận thủ giữa chương trình và đặc tả của nó, các kết quả được trình bày trong các Chương 5 và 6. Chương 5 trình bày phương pháp kiểm chứng sự tuân thủ giữa sự cài đặt của chương trình tương tranh so với đặc tả giao thức tương tác của nó. Chương 6 trình bày phương pháp kiểm chứng các ràng buộc thời gian giữa các thành phần tuần tự và song song trong chương trình tương tranh.2 – Cấu trúc luận án. z Chương 2 Kiến thức cơ sở 2.1 Kiểm chứng phần mềm Kiểm chứng phần mềm (software verification) là tập các nguyên lý, phương pháp và công cụ để bảo đảm tính đúng đắn của các sản phẩm phần mềm.
Trong mục này chúng tôi giới thiệu tổng quan về hai phương pháp kiểm chứng phần mềm là các phương pháp kiểm chứng hình thức và kiểm chứng tại thời điểm thực thi chương trình.1 Kiểm chứng hình thức 2.1 Kiểm chứng mô hình Phương pháp kiểm chứng mô hình (model checking) được sử dụ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 phần mềm cho trước. Cho 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, ký hiệu M |= p [19]. Về mặt thực thi, kiểm chứng mô hình sẽ duyệt qua 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. Trong đó, các thuộc tính được đặc tả bằng logic thời gian LTL hoặc CTL [19].
Mô hình M là 9 z Chương 2. Kiến thức cơ sở 10 Bảng 2.1 – Chứng minh định lý P1 , P2 , ., Pn ` name C một cấu trúc Kripke gồm bốn thành phần M = (S , S0 , L, R) với S là một tập hữu hạn các trạng thái, S0 ∈ S là trạng thái đầu, R ⊂ S ×S là quan hệ chuyển trạng thái, L : S → 2AP là hàm gán nhãn với AP là tập hữu hạn các mệnh đề nguyên tử được xây dựng từ hệ thống. Một bộ kiểm chứng mô hình [16, 56] (model checker ) sẽ kiểm tra tất cả các trạng thái có thể có của mô hình để tìm ra tất cả các đường thực thi có thể gây ra lỗi. Do đó không gian trạng thái thường là vô cùng lớn nếu không muốn nói là vô hạn.
Vì vậy việc phải duyệt qua tất cả các trạng thái là bất khả thi. Để đối phó với bài toán bùng nổ không gian trạng thái đã có một vài nghiên cứu liên quan đến các kỹ thuật làm giảm không gian trạng thái như Abstraction, Slicing [35, 80].2 Chứng minh định lý Phương pháp chứng minh định lý (theorem proving) [20] sử dụng các kĩ thuật suy luận để chứng minh tính đúng đắn của một công thức hay tính khả thỏa của một công thức F với tất cả các mô hình, ký hiệu |= F. Một hệ chứng minh bao gồm các luật suy diễn có dạng như trong Bảng 2. Trong đó, Pi với i = 1.n là tập các tiên đề, C là tập các định lý.
Một hệ thống được gọi là đúng (sound ) nếu tất cả các định lý của nó đều được chứng minh. Các phương pháp chứng minh định lý như B [5], Event-B [8] đã được sử dụng thành công để đặc tả và kiểm chứng tính đúng đắn của mô hình thiết kế phần mềm.4 chúng tôi trình bày chi tiết về một phương pháp chứng minh định lý với Event-B, phương pháp này sẽ được sử dụng để kiểm chứng tính đúng đắn của bản thiết kế các chương trình tương tranh. Kiến thức cơ sở 11 2.2 Kiểm chứng tại thời điểm thực thi Kiểm chứng tại thời điểm thực thi [18] (runtime verification) là kỹ thuật kết hợp giữa kiểm chứng hình thức và thực thi chương trình để phát hiện các lỗi của hệ thống dựa trên quá trình quan sát input/output khi thực thi chương trình. Các hành vi quan sát được như bản ghi của các vết (log of traces) được theo dõi và kiểm tra tính khả thỏa với đặc tả yêu cầu hệ thống.
Các yêu cầu có thể được đặc tả bằng logic thời gian (linear temporal logic), automát,. So với phương pháp kiểm chứng tĩnh thì kiểm chứng tại thời điểm thực thi được thực hiện trong khi thực thi hệ thống. Do đó, phương pháp này còn được gọi là kiểm thử bị động (passive testing). Kiểm chứng tại thời điểm thực thi nhằm bảo đảm sự tuân thủ giữa cài đặt hệ thống phần mềm so với đặc tả thiết kế của nó.
Các lý do sau được lựa chọn khi sử dụng phương pháp kiểm chứng tại thời điểm thực thi. Không thể bảo đảm tính đúng đắn giữa sự cài đặt của chương trình so với đặc tả thiết kế của nó, 2. Nhiều thông tin chỉ sẵn có hoặc thuận tiện ở thời điểm thực thi chương trình, 3. Các hành vi của hệ thống có thể phụ thuộc vào môi trường khi nó được thực thi, 4.
Với các hệ thống an toàn và bảo mật cao thi việc giám sát các hành vi hoặc thuộc tính đã được thử nghiệm hoặc chưng minh bằng các phương pháp tĩnh là cần thiết.2 Một số vấn đề trong chương trình tương tranh Trong các chương trình tương tranh, có hai thuộc tính cơ bản cần phải bảo đảm là an toàn (safety) và thực hiện được (liveness) [65, 73]. Thuộc tính an toàn bảo đảm chương trình luôn thỏa mãn (luôn đúng) các ràng buộc của nó. Ví dụ như ràng buộc về sự xung đột (interference) giữa các tiến trình. Thuộc tính thực hiện được bảo đảm chương trình cuối cùng sẽ thỏa mãn (sẽ đúng) các ràng buộc của nó.
Ví dụ như tính dừng của các tiến trình (process termination) và các tiến trình z Chương 2. Kiến thức cơ sở 12 khi muốn truy cập vào tài nguyên chia sẻ (shared resource) thì cuối cùng nó sẽ truy cập được. Một số vấn đề về tương tranh liên quan đến hai thuộc tính này được mô tả như sau. Sự xung đột (interference) xảy ra khi hai hoặc nhiều tiến trình đồng thời truy cập một biến chia sẻ, trong đó có ít nhất một tiến trình ghi và các tiến trình khác không có cơ chế rõ ràng để ngăn chặn sự truy cập đồng thời này.
Khi đó giá trị của biến chia sẻ và kết quả của chương trình sẽ phụ thuộc vào sự đan xen (interleaving) hay thứ tự thực hiện của các tiến trình. Sự xung đột còn được gọi là cạnh tranh dữ liệu (data race). Tắc nghẽn xảy ra khi hệ thống (chương trình) không thể đáp ứng được bất kỳ tín hiệu hoặc yêu cầu nào. Có hai dạng tắc nghẽn, dạng một xảy ra khi các tiến trình dừng lại và chờ đợi lẫn nhau, ví dụ một tiến trình nắm giữ một khóa mà các tiến trình khác mong muốn và ngược lại.
Dạng hai xảy ra khi một tiến trình chờ đợi một tiến trình khác không kết thúc. Một thuộc tính khác tương tự như khóa chết khi các tiến trình liên tục thay đổi trạng thái của nó để đáp ứng với những thay đổi của các tiến trình khác mà không đạt được mục đích cuối cùng. Sự đói (starvation) liên quan đến sự tranh chấp tài nguyên, vấn đề này xảy ra khi một tiến trình không thể truy cập đến các tài nguyên chia sẻ.3 Sự tương tranh trong Java Java là ngôn ngữ lập trình hướng đối tượng hỗ trợ lập trình tương tranh với cơ chế đồng bộ hóa giữa các tiến trình, mô hình bộ nhớ chia sẻ, môi trường lập trình trực quan và thư viện phong phú với nhiều giao diện lập trình tương tranh khác nhau. Java được biết đến như một ngôn ngữ lập trình tương tranh được sử dụng rộng rãi trong công nghiệp phần mềm.
Sự tương tranh trong Java [82] được thực hiện thông qua cơ chế giám sát các tiến trình, hành vi của tiến trình được mô tả trong phương thức run. Sự thực thi của một tiến trình có thể được điều khiển bởi các tiến trình khác thông qua các z Chương 2. Kiến thức cơ sở 13 phương thức stop, suspend và resum. Tuy nhiên, với các hệ thống lớn gồm nhiều tiến trình thì sử dụng các phương thức này để điều khiển sự thực thi của các tiến trình là không an toàn, do chúng ta khó kiểm soát tất cả các tiến trình.
Do đó, Java cung cấp một mô hình tương tranh để giải quyết sự đồng bộ hóa giữa các tiến trình. Khi nhiều tiến trình cùng muốn truy cập vào dữ liệu chia sẻ trong một vùng giới hạn được đánh dấu bằng từ khóa synchoronized thì tại một thời điểm khóa của vùng xung đột chỉ cho phép một tiến trình được phép truy cập. Một tiến trình sẽ sử dụng phương thức wait để chờ khi nó không thể truy cập vào vùng xung đột mà đã bị chiếm giữ bởi tiến trình khác. Các tiến trình có thể được đánh thức bằng các phương thức notify hoặc notifyAll.
Chiến lược giám sát ở mức thấp của Java không tránh được các lỗi liên quan về tương tranh như khóa chết, xung đột. Trong các mục tiếp theo của chương này, luận án trình bày một số mô hình và công cụ để đặc tả và kiểm chứng các thành phần Java tương tranh.1 Mô hình lưu trữ (JMM-Java Memory Model) Trong Java, các tiến trình tương tác với nhau thông qua việc đọc ghi dữ lệu chia sẻ. Mô hình lưu trữ JMM [46] biểu diễn sự tương tác giữa các tiến trình trong bộ nhớ. Trong đó, mỗi tiến trình sẽ gọi các hành động sau.
– use đọc một vùng nhớ (region) trong bộ nhớ làm việc (working memory), – assign ghi vào vùng nhớ đã được đọc trong bộ nhớ làm việc, – read bắt đầu đọc dữ liệu từ bộ nhớ chính của vùng nhớ, – load kết thúc việc đọc dữ liệu từ bộ nhớ chính của vùng nhớ, – store bắt đầu ghi dữ liệu từ bộ nhớ làm việc vào bộ nhớ chính của vùng nhớ, – write kết thúc việc ghi dữ liệu từ bộ nhớ làm việc vào bộ nhớ chính của vùng nhớ, – lock lấy giá trị trong bộ nhớ chính và chuyển giao cho một tiến trình đang làm việc trong bộ nhớ thông qua các hành động read và load, – unlock đẩy các giá trị của một tiến trình đang lắm giữ trong bộ nhớ làm việc vào bộ nhớ chính thông qua các hành động store và write. Kiến thức cơ sở 14 JMM định nghĩa các luật về sự tương tác giữa các tiến trình và các hành vi của chương trình Java tương tranh, do đó người lập trình có thể thiết kế và cài đặt chương trình một cách đúng đắn và phù hợp.