CHƯƠNG 1 – GIỚI THIỆU CHUNG 1. Giới thiệu về VDM 1. Khái niệm Phương pháp phát triển Vienna (Vienna Development Method) là một trong những phương pháp mô hình hóa hướng đối tượng lâu đời nhất cho việc phát triển phần mềm. Nó bao gồm một nhóm các ngôn ngữ trên nền tảng toán học và các công cụ hỗ trợ việc mô tả và phân tích mô hình hệ thống tại bước thiết kế.
Việc xây dựng và phân tích mô hình giúp cho việc nhận biết những đặc tả của hệ thống còn thiếu sót hoặc chưa rõ ràng, và đảm bảo một mức độ tin tưởng trong quá trình phát triển, đặc biệt là vấn đề an toàn và bảo mật. VDM đã được ứng dụng nhiều trong công nghiệp, trong một số trường hợp, người sử dụng không phải là những chuyên gia trong các lĩnh vực chuyên nghiệp và logic. Theo kinh nghiệm cho thấy, việc mô hình hóa sẽ làm tăng chi phí ở giai đoạn thiết kế, nhưng nó có thể giúp rút ngắn giai đoạn phát triển nhờ việc hạn chế công sức làm lại do những lỗi trong giai đoạn thiết kế [6]. Mô hình hóa cấu trúc (Modeling structure) Trong VDM, mô hình bao gồm việc mô tả dữ liệu trên các phương thức và chức năng của hệ thống mà nó được thực thi.
Dữ liệu bao gồm việc nhập/xuất từ bên ngoài và dữ liệu trạng thái bên trong. Chức năng bao gồm các hoạt động có thể được gọi tại giao diện hệ thống cũng như các chức năng phụ, hỗ trợ việc thực hiện các hoạt động. Trong chuẩn ISO, có một thông tin bổ sung về framework cho việc mô hình hóa – VDM-SL. Ngôn ngữ VDM++ mở rộng của VDM-SL, được dùng để hỗ trợ đặc tả hệ thống hướng đối tượng, và mô hình cấu trúc trong những định nghĩa class, mỗi class có những thành phần tương tự một đặc tả VDM-SL, với các biến trạng thái đóng vai trò của biến thể hiện và các hoạt động đóng vai trò là một phần của các phương thức.
Mô hình hóa dữ liệu (Modeling data) Các mô hình dữ liệu trong VDM được thành lập dựa trên các kiểu dữ liệu trừu tượng cơ bản cùng với một tập hợp các kiểu khởi tạo. Các kiểu dữ liệu cơ bản bao gồm kiểu số (tự nhiên, số nguyên, số hữu tỉ và số thực) và kiểu ký tự. Chú ý, trong nguyên tắc trừu tượng của VDM thì không xác định giá trị lớn nhất cho kiểu số hoặc kiểu số thực. Nếu người dùng muốn xác định bởi yêu cầu của việc mô hình hóa, thì có thể xác định điều này bằng việc quy định tính bất biến (invariant).
Bất biến là các biểu thức logic đại diện cho các điều kiện được tôn trọng bởi các tất cả các thành phần kiểu dữ liệu mà chúng đính kèm [6]. LUAN VAN CHAT LUONG download : add luanvanchat@agmail. Các loại VDM Phương thức phát triển Vienna (Vienna Development Method - VDM) được phát triển đầu tiên bởi IBM vào năm 1970, là một trong những phương pháp hình thức được thành lập lâu nhất. VDM có 3 loại: VDM-SL (VDM Specification Language) một chuẩn ISO; VDM++ một mở rộng hướng đối tượng của VDM-SL; và mới đây thêm VDM-RT, một mở rộng của VDM++ để mô hình hóa những hệ thống nhúng phân tán thời gian thực.
VDM-RT là một ngôn ngữ mô hình hóa với những tập con có thể thực thi được sử dụng để miêu tả những hệ thống nhúng thời gian thực phân tán [9,1]. - VDM-SL: Đặc tả VDM-SL có cấu trúc rất đơn giản, đó là Module, mang tính diễn tả bài toán bằng Structure. Một module bao gồm một tập của types, constants, functions, operations và state (trạng thái). Diễn tả bài toán dạng module, một module bao gồm một tập của types, constants, functions, operations và state (trạng thái).
Phù hợp với bài toán phân tích theo cấu trúc, theo module và cài đặt ngôn ngữ lập trình kiểu cấu trúc. - VDM++: Đặc tả VDM++ là mở rộng của VDM-SL có cấu trúc dựa trên class, làm việc với diễn tả bài toán thông qua Class, hướng đối tượng. Một class bao gồm một tập hợp của types, constants, functions, operations và state. Phù hợp phân tích hướng đối tượng.
- VDM-RT: Đặc tả VDM-RT là VDM++ với hệ thống có môi trường rằng buộc, áp dụng vào hệ thống nhúng thời gian thực và hệ thống phân tán. Điểm khác biệt chính giữa VDM-SL và VDM++ là cách thức mà cấu trúc được xử lý. VDM-SL có một phần mở rộng mô-đun thông thường, trong khi đó VDM++ có một cơ chế cấu trúc hướng đối tượng truyền thống với các class và sự thừa kế [10]. VDM ++ Một mô hình VDM++ bao gồm một tập các class.
Một class mô tả một tập các đối tượng có các thành phần dùng chung như thuộc tính hoặc phương thức. Mô tả class cung cấp một khuôn mẫu cho các đối tượng được tạo ra từ class đó. Một số thành phần sẽ được nhìn thấy bởi các đối tượng khác và một số thành phần chỉ được sử dụng bởi chính đối tượng đó, điều này được khai báo bằng cách sử dụng phạm vi truy cập [12]. Cấu trúc class Cấu trúc của một class được mô tả như dưới đây.
Trong một class bao gồm nhiều khối, mỗi khối được bắt đầu bởi một từ khóa chỉ ra loại các thành phần trong khối đó. Mọi thành phần được định nghĩa trong một khối được coi như một thành phần của class. Các khối được mô tả như sau: Biến thể hiện (Instance variables): mô hình trạng thái của một đối tượng. Kiểu (Types): định nghĩa các kiểu dữ liệu dùng cho đối tượng.
Giá trị (Values): định nghĩa các hằng số. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 12 Hàm (Functions): định nghĩa các hàm mà không tác động đến các biến. Phương thức (Operations): định nghĩa các phương thức có thể thay đổi giá trị các biến. Khi một đối tượng là chủ động, nó có 1 luồng để khai báo tính chủ động, đối tượng này sẽ được gọi khi bắt đầu một luồng xử lý.
Ràng buộc đồng bộ (Synchronisation constraints): VDM++ hỗ trợ mô hình hóa một hệ thống phần mềm đồng thời (concurrent software system), điều này có nghĩa là một đối tượng có thể tồn tại đồng thời và hoạt động song song. Khối này xác định sự ràng buộc trong việc trao đổi giữa những đối tượng đồng thời được ràng buộc. class class-name instance variables Internal object state. types values functions Definitions operations.
thread Dynamic behaviour. sync Synchronization control. end class-name Hình 1. Cấu trúc class trong VDM++ Giữa các lớp có những mối quan hệ kế thừa, lớp kế thừa được gọi là subclass và lớp được kế thừa được gọi là superclass.
Định nghĩa lớp kế thừa sẽ được mở rộng với các thành phần của lớp cha (được kế thừa) mà cho phép kế thừa bằng cách khai báo là public hoặc protected. Một class có thể kế thừa một hoặc nhiều lớp. Có một giới hạn trọng việc đa thừa kế là chỉ duy nhất một lớp cha có khai báo luồng. Cấu trúc một lớp thừa kế như dưới đây: LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 13 class class name is subclass of sc1, sc2,.
end class name Hình 1. Cú pháp khai báo lớp thừa kế 1. Phạm vi truy cập (Access Modifier) Mỗi khai báo thành phần bên trong một class có thể có một phạm vi truy cập. Trong VDM++ có 3 loại phạm vi truy cập là: private, protected và public.
Phạm vi truy cập mặc định của tất cả các thành phần là private. Phạm vi truy cập không thể được giới hạn lại ở các lớp kế thừa. Ví dụ, một lớp kế thừa không thể ghi đè phạm vi truy cập của một phương thức ở lớp cha được khai báo public thành private. Static có thể được sử dụng để khai báo các biến độc lập với một thể hiện cụ thể của lớp.
Biến static có thể được truy cập thông qua tên class thay vì thông qua một thể hiện của class. Một thành phần static (tĩnh) của class không cho phép các thành phần không phải static truy cập. Trong VDM++ thì khối value và type mặc định là static. Hàm khởi tạo (Constuctors) Mỗi class có thể có một số hàm khởi tạo.
Hàm khởi tạo được phân biệt với các hàm khác bằng tên class và kiểu trả về tương tự. Việc trả về kết quả không cần phải rõ ràng và hàm khởi tạo sẽ được gọi khi một thể hiện của lớp được tạo mới. Biến thể hiện (Instance Variables) Trạng thái của một đối tượng được mô hình hóa bằng ý nghĩa của các biến thể hiện. Khối định nghĩa các biến thể hiện trong một class có định dạng như sau: class class name instance variables instance variable definition 1; instance variable definition 2;.
instance variable definition n end class name Hình 1. Cú pháp khai báo biến thể hiện LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 14 Tính đồng nhất của các thuộc tính được mô hình hòa là bất biến (invariant) trong VMD++. Trong trường hợp cần giới hạn giá trị cho các biến thể hiện hoặc quy định mối liên hệ giữa chúng thì VDM++ hỗ trợ việc khai báo rằng buộc đối với các giá trị của biến thể hiện. Một định nghĩa bất biến theo ngay sau khai báo biến thể hiện, có cấu trúc như sau: class class name instance variables instance variable definition 1; instance variable definition 2;.
instance variable definition n; inv expression using the instance variables end class name Hình 1. Cú pháp khai báo tính bất biến Ví dụ, ta định nghĩa một class mô hình hóa một đối tượng người, với các thuộc tính là tên và tuổi. Trong đó, tuổi phải đảm bảo rằng buộc là lớn hoặc bằng không tuổi và không lớn hơn 99 tuổi. Điều này có thể được định nghĩa như sau: class Person types string = seq of char instance variables name: string := []; age: int := 0; inv 0 <= age and age <= 99; end Person Hình 1.
Ví dụ khai báo rằng buộc biến thể hiện bằng biểu thức INV Thuộc tính bất biến này có hiệu lực tại mọi thời điểm đối với các thể hiện của lớp. Mọi việc gán giá trị mới cho biến điều phải được kiểm tra thỏa mãn rằng buộc đã khai báo. Bằng việc khai báo tính bất biến của các biến thể hiện, VDM++ đã cho phép mô hình hóa các rằng buộc của các thuộc tính của hệ thống phần mềm trong quá trình thiết kế hệ thống. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 15 Biến thể hiện chỉ có thể được truy cập bởi các thành phần trong class nó khai báo.
Để đọc hoặc thay đổi giá trị của biến thể hiện từ bên ngoài class, cần phải khai báo các phương thức truy cập. Ví dụ, để lấy tên của một người, ta khai báo hàm GetName như sau: class Person. instance variables name: string := [];. operations public GetName: () ==> string GetName () == return name end Person Hình 1.