Đặt vấn đề Trong thời đại ngày nay, các hệ thống có yếu tố thời gian và đặc biệt các hệ thống thời gian thực là một trong những lĩnh vực nhận được rất nhiều sự quan tâm của giới khoa học nói chung và giới khoa học nghiên cứu về công nghệ nói riêng. Thật vây, hệ thống thời gian thực được ứng dụng rất nhiều trong đời sống xã hội, trong sản xuất, trong y tế, trong hàng không vũ trụ và trong quân sự, gần như trong mọi lĩnh vực ta đều thấy có sự góp mặt của những ứng dụng trong hệ thống thời gian thực. Không chỉ góp mặt trong nhiều lĩnh vực mà sự góp mặt của nó còn có tầm quan trọng rất lớn đối với hệ thống. Trong hệ thống thời gian thực, các công vệc và các tác vụ cần phải hoàn thành trong một khoảng thời gian cho phép (deadline), nếu không đáp ứng được yêu cầu thời gian thì hệ thống sẽ sụp đổ hoặc sẽ gây ra hậu quả nghiêm trọng (hệ thời gian thực cứng: Hard Real- Time) hoặc sẽ bị suy giảm về chất lượng dịch vụ (hệ thời gian thực mềm: Soft Real-Time) [6, 9].
Chính vì tầm quan trọng của yếu tố thời gian trong hệ thống thời gian thực như vậy nên việc kiểm tra tính đúng đắn đối với hệ thống này là rất cần thiết. Việc kiểm tra tính đúng đắn của một hệ thống có thể được thực hiện ở khâu kiểm thử và kiểm chứng. Tuy nhiên, với những hệ thống có ràng buộc về thời gian cũng như tầm quan trọng của hệ thống mà việc kiểm thử không kiểm tra được hết mà chủ yếu tập chung ở khâu kiểm chứng [10]. Việc kiểm chứng tính đúng đắn của hệ thống nhằm kiểm tra xem hệ thống có vận hành đúng như yêu cầu không, muốn vậy cần phải có mô phỏng sự vận hành của hệ thống, cần có bước kiểm tra quy trình vận hành đó có đảm bảo các tính chất cơ bản của một hệ thống như: tính đến được của một trạng thái, tính an toàn, tính liên tục theo thời gian (không bị dừng – not deadlock) [10, 11].
Muốn làm được điều đó cần phải có một bộ công cụ có thể mô tả được sự vận hành của hệ thống, qua đó mô phỏng được sự vận hành đó và từ đó kiểm tra được sự vận hành đó có thỏa mãn các yêu cầu của hệ thống hay không. Đây thực sự là mối quan tâm lớn đối với vấn đề kiểm chứng nói riêng và công nghệ phần mềm nói chung. Hiện nay có rất nhiều bộ công cụ cho phép kiểm chứng tự động các hệ thống phần mềm có yếu tố thời gian như: SPIN, LTSmin, mCRL2, MRMC, PAT, TAPAL, DREAM, ROMEO, UPPAAL … Trong đó bộ công cụ Uppaal thể hiện 2 những tính năng mạnh mà những bộ công cụ khác không có như việc mô phỏng được sự vận hành của hệ thống thời gian thực và kiểm chứng sự vận hành bởi các hệ thống câu lệnh rất đơn giản. Công cụ này giúp ta có thể kiểm chứng những hệ thống được mô hình hóa thành những hệ thống ô-tô-mát thời gian với nhứng biến số nguyên, cấu trúc dữ liệu, hàm người dùng và đồng bộ các kênh.
Với việc đặc tả và kiểm chứng một hệ thống thời gian thực thì bộ công cụ Uppaal được đánh giá là tốt nhất hiện nay và được sử dụng rộng rãi trong công nghiệp. Nhưng bên cạnh đó việc sử dụng bộ công cụ Uppaal trong kiểm chứng hệ thống có yếu tố thời gian cũng đòi hỏi người sử dụng có trình độ nhất định trong việc đặc tả hệ thống dưới dạng các ô-tô-mát thời gian cũng như điều khiển sự vận hành và tương tác giữa các ô-tômát đó thông qua một ngôn ngữ lập trình [7, 8].2 Mục tiêu và phạm vi của đề tài Trong luận văn này tác giả đã tập trung tìm hiểu về bộ công cụ kiểm chứng Uppaal, đi sâu vào tìm hiểu ngôn ngữ đặc tả của Uppaal, tìm hiểu cách đặc tả một hệ thống phần mềm dưới dạng các ô-tô-mát thời gian và điều khiển sự vận hành của hệ thống thông qua ngôn ngữ lập trình C++, cũng như tìm hiểu cơ chế kiểm chứng của bộ công cụ này cho các hệ thống thời gian thực. Từ đó tác giả xây dựng một số ví dụ (cụ thể tác giả đã xây dựng được 4 ví dụ) về một số hệ thống thời gian thực áp dụng vào đặc tả và kiểm chứng hệ thống đó bởi bộ công cụ Uppaal. Đối với mỗi ví dụ tác giả giả định là một hệ thống thời gian thực, tiến hành đặc tả, mô hình hóa dưới hệ ô-tô-mát thời gian trên trình soạn thảo của Uppaal sau đó chạy mô phỏng và kiểm chứng sự hoạt động của hệ thống đó.3 Cấu trúc của luận văn Phần còn lại của luận văn được trình bày thành ba chương: Ở chương 2, tác giả trình bày những cơ sở lí thuyết cần thiết cho việc nghiên cứu đề tài.
Sang chương 3, tác giả nêu những hiểu biết của tác giả về bộ công cụ Uppaal cũng như cách đặc đả một hệ thống phần mềm dưới dạng các ô-tô-mát thời gian và phương pháp mô phỏng và kiểm chứng trong Uppaal. Chương 4, tác giả trình bày một số ví dụ áp dụng mà tác giả đã xây dựng được sau khi tìm hiểu về bộ công cụ Uppaal. Chương này tác giả trình bày bốn ví dụ mà tác giả đã xây dựng được về bốn hệ thống thời gian và tiến hành đặc tả và kiểm chứng các hệ thống đó qua công cụ Uppaal. Cuối cùng là phần kết luận, ở đây tác giả tóm tắt những công việc mà tác 3 giả đã làm được trong luận văn cũng như đưa ra những hạn chế và hướng mở rộng tiếp theo của đề tài.1 Đặc tả hệ thống Dựa trên những yêu cầu đối với việc sử dụng hệ thống để đưa ra các đặc tả cho hệ thống.
Muốn đặc tả tốt hệ thống thì người đặc tả cần hiểu rõ nguồn gốc, các dạng thông tin cần cung cấp cho hệ thống hoạt động, cần nắm được hệ thống sẽ phải giải quyết những vấn đề gì, những kết quả cần phải có khi vận hành hệ thống là gì. Xác định được mối quan hệ giữa cái vào và cái ra cho quá trình hoạt động của hệ thống. Các đặc tả chi tiết hệ thống nhằm phục vụ cho việc xây dựng và trắc nghiệm về hệ thống để kiểm tra xem những nhiệm vụ đã đặt ra cho hệ thống có hoàn tất được hay không [5]. Việc sử dụng ngôn ngữ tự nhiên để đặc tả hệ thống dẫn đến rất nhiều bất tiện trong đó nhữn bất tiện tiêu biểu có thể kể đến như: Việc nhầm lẫn do cách hiểu các khái niệm khác nhau giữa hai bên; Đặc tả yêu cầu ngôn ngữ tự nhiên quá mềm dẻo do đó một vấn đề có thể được mô tả bằng quá nhiều cách khác nhau; Các yêu cầu không được phân hoạch tốt, khó tìm các mối quan hệ Do vậy người ta thường dùng các thay thế khác để đặc tả các yêu cầu như: Đặc tả bằng ngôn ngữ tự nhiên có cấu trúc; đặc tả bằng ngôn ngữ mô tả thiết kế, giống ngôn ngữ lập trình nhưng có mức trừu tượng cao hơn; Đặc tả bằng ngôn ngữ đặc tả yêu cầu; Đặc tả bằng ghi chép graphic; Đặc tả toán học,.
Đặc tả hệ thống có thể chia thành hai loại: đặc tả phi hình thức (ngôn ngữ tự nhiên) và đặc tả hình thức (dựa trên kiến trúc toán học). Đặc tả phi hình thức: Đặc tả phi hình thức là đặc tả sử dụng ngôn ngữ tự nhiên. Như đã trình bày ở trên, đặc tả theo hình thức này có thể không được chặt chẽ nhưng nhiều người có thể dễ dàng tiếp cận và có thể dùng để trao đổi với nhau để làm chính xác hóa các điểm chưa rõ, chưa thống nhất giữa các bên phát triển hệ thống. Đặc tả hình thức: Đặc tả hình thức là đặc tả mà ở đó các từ ngữ, cú pháp, ngữ nghĩa được định nghĩa hình thức dựa vào toán học.
Đặc tả hình thức có thể coi là một phần của hoạt động đặc tả phần mềm. Với hình thức đặc tả này các đặc tả yêu cầu được phân tích một cách chi tiết, các mô tả trừu tượng của các chức năng chương trình có thể được tạo ra để làm rõ yêu cầu. 5 Đối với nhữn hệ thống tương đối phức tạp, có hai hướng tiếp cận đặc tả hình thức để phát triển các hệ thống đó là: Hướng tiếp cận đại số, hệ thống được mô tả dưới dạng các toán tử và các quan hệ và hướng tiếp cận mô hình, mô hình hệ thống được cấu trúc sử dụng các thực thể toán học như là các tập hợp và các thứ tự. Việc sử dụng đặc tả hình thức để đặc tả một hệ thống mang lại nhiều thuận lợi.
Thứ nhất đặc tả hình thức cho phép chúng ta thấy và hiểu được bản chất bên trong của các yêu cầu, đây chính là cách tốt nhất để làm giảm các lỗi, các thiếu sót có thể xảy ra ngay từ bước đầu và giúp cho công việc thiết kế được thuận lợi. Thứ hai do sử dụng suy luận toán học cho việc đặc tả nên có thể dựa vào các công cụ toán học khi phân tích và điều này làm tăng thêm tính chắc chắn và tính đầy đủ của hệ thống và cuối cùng việc đặc tả hình thức một hệ thống đem lại một cách thức cho việc kiểm tra hệ thống đó một cách thuận tiện. Việc đặc tả một hệ thống cần đảm bảo những nguyên tắc: Phân tách chức năng với cài đặt; đặc tả hệ thống hướng tiến trình; đặc tả hệ thống phải là một mô hình nhận thức; đảm bảo đặc tả mô tả được sự vận hành của hệ thống; khi đặc tả phải tính toán đến khả năng không đầy đủ do môi trường phức tạp và cuối cùng việc đặc tả phải cục bộ và lỏng lẻo để thuận tiện cho việc thay đổi phát sinh.2 Kiểm chứng hệ thống phần mềm Kiểm chứng hệ thống phần mềm thực hiện việc xác minh một thiết kế hay một sản phẩm phần mềm thỏa mãn những những thuộc tính được nêu ra trong đặc tả của hệ thống [5]. Đặc tả hệ thống trở thành cơ sở của mọi hoạt động kiểm chứng.
Một thiếu sót sẽ được phát hiện khi hệ thống không thỏa mãn một trong các thuộc tính đã được đặc tả. Hệ thống được xác minh là đúng khi nó thỏa mãn tất cả các thuộc tính mà nó đã được đặc tả. Quy trình kiểm chứng hệ thống được thể hiện thông qua sơ đồ (xem hình 2.
