Luận văn thạc sĩ vnu uet nghiên cứu và ứng dụng vdm cho mô hình hóa và kiểm thử hệ thống imp tại nttdata việt nam

Luận văn thạc sĩ nghiên cứu vnu uet nghiên cứu và ứng dụng vdm cho mô hình hóa và kiểm thử hệ thống imp tại nttdata việt nam, khảo sát thực trạng, phân tích nguyên nhân, đề xuất

• Tác giả: Nguyễn Xuân Tùng
• Người hướng dẫn: TS. Nguyễn Văn Tăng
• Trường học: Trường Đại Học Công Nghệ - Đại Học Quốc Gia Hà Nội
• Chuyên ngành: Công Nghệ Thông Tin
• Đề tài: Nghiên cứu và ứng dụng VDM++ cho mô hình hóa và kiểm thử hệ thống IMP tại NTTDATA Vietnam
• Loại tài liệu: Luận văn thạc sĩ
• Năm xuất bản: 2015
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CẢM ƠN
• LỜI CAM ĐOAN
• 1. CHƯƠNG 1: GIỚI THIỆU CHUNG
• 1.1. Giới thiệu về VDM
• 1.2. Cấu trúc class
• 1.3. Hàm khởi tạo (Constuctors)
• 1.4. Biến thể hiện (Instance Variables)
• 1.5. Hàm và Phương thức
• 1.6. Tính đồng thời (Concurrency)
• 1.7. Công cụ hỗ trợ VDM++
• 2. CHƯƠNG 2: TỔNG QUAN VỀ DỰ ÁN
• 2.1. Giới thiệu về dự án
• 2.2. Hiện trạng nghiệp vụ
• 2.3. Mục đích xây dựng hệ thống IMP
• 2.4. Hệ thống IMP
• 2.5. Nền tảng hệ thống
• 2.6. Luồng nghiệp vụ hệ thống
• 2.7. Quy trình phát triển dự án
• 2.8. Quy trình phát triển hiện tại
• 2.9. Đánh giá vấn đề của dự án
• 2.10. Giải pháp tổng thể
• 3. CHƯƠNG 3: ÁP DỤNG QUY TRÌNH MỚI VÀO DỰ ÁN IMP
• 3.1. Mô hình hóa thực thể dữ liệu
• 3.2. Mô hình hóa kiểu dữ liệu SQL
• 3.3. Mô hình hóa cấu trúc bảng
• 3.4. Mô hình hóa bảng dữ liệu
• 3.5. Mô hình hóa cơ sở dữ liệu
• 3.6. Mô hình hóa đặc tả hệ thống
• 3.7. Đặc tả kiến trúc
• 3.8. Đặc tả nghiệp vụ
• 3.9. Kiểm thử mô hình hóa
• 3.10. Kết quả thực nghiệm
• 3.11. Kinh nghiệm thực tiễn
• KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng quan về Nghiên cứu VDM cho mô hình hóa hệ thống IMP

Nghiên cứu về VDM++ đã trở thành một phần quan trọng trong việc mô hình hóa và kiểm thử hệ thống tại NTTDATA Việt Nam. VDM++ là một ngôn ngữ mô hình hóa hướng đối tượng, giúp các nhà phát triển có thể mô tả và phân tích các hệ thống phức tạp một cách chính xác. Việc áp dụng VDM++ trong mô hình hóa hệ thống IMP không chỉ giúp cải thiện chất lượng thiết kế mà còn giảm thiểu rủi ro trong quá trình phát triển phần mềm.

1.1. VDM là gì và ứng dụng của nó trong mô hình hóa

VDM++ (Vienna Development Method) là một ngôn ngữ mô hình hóa hướng đối tượng, được sử dụng để mô tả các hệ thống phần mềm. Ngôn ngữ này cho phép các nhà phát triển xác định các yêu cầu và đặc tả hệ thống một cách rõ ràng, từ đó giúp phát hiện lỗi sớm trong quá trình phát triển.

1.2. Tại sao chọn VDM cho hệ thống IMP tại NTTDATA

Hệ thống IMP tại NTTDATA Việt Nam yêu cầu một phương pháp mô hình hóa mạnh mẽ để đảm bảo tính chính xác và hiệu quả. VDM++ cung cấp các công cụ và kỹ thuật cần thiết để mô hình hóa các yêu cầu phức tạp, từ đó giúp cải thiện quy trình phát triển và kiểm thử phần mềm.

II. Thách thức trong mô hình hóa và kiểm thử hệ thống IMP

Mô hình hóa và kiểm thử hệ thống IMP gặp phải nhiều thách thức, bao gồm việc xác định các yêu cầu không rõ ràng và phát hiện lỗi trong giai đoạn thiết kế. Những vấn đề này có thể dẫn đến việc phát triển không đúng yêu cầu và tăng chi phí cho dự án.

2.1. Các vấn đề thường gặp trong quy trình phát triển

Trong quy trình phát triển phần mềm, việc thiếu sót trong việc xác định yêu cầu có thể dẫn đến những lỗi nghiêm trọng. Các nhà phát triển thường gặp khó khăn trong việc hiểu rõ các yêu cầu của khách hàng, dẫn đến việc thiết kế không chính xác.

2.2. Tác động của lỗi thiết kế đến dự án

Lỗi thiết kế không chỉ ảnh hưởng đến chất lượng sản phẩm mà còn làm tăng thời gian và chi phí phát triển. Việc phát hiện lỗi muộn trong quy trình phát triển có thể dẫn đến việc phải làm lại nhiều công đoạn, gây lãng phí tài nguyên.

III. Phương pháp áp dụng VDM trong mô hình hóa hệ thống IMP

Áp dụng VDM++ vào mô hình hóa hệ thống IMP giúp cải thiện quy trình phát triển và kiểm thử. Phương pháp này cho phép các nhà phát triển mô tả rõ ràng các yêu cầu và đặc tả hệ thống, từ đó phát hiện lỗi sớm và giảm thiểu rủi ro.

3.1. Quy trình mô hình hóa với VDM

Quy trình mô hình hóa với VDM++ bao gồm việc xác định các yêu cầu, xây dựng mô hình và kiểm thử. Các nhà phát triển sử dụng VDM++ để tạo ra các mô hình chính xác, từ đó giúp phát hiện lỗi và cải thiện chất lượng sản phẩm.

3.2. Kiểm thử tự động với VDM

Kiểm thử tự động là một phần quan trọng trong quy trình phát triển phần mềm. VDM++ hỗ trợ việc kiểm thử tự động thông qua việc mô hình hóa các yêu cầu và đặc tả hệ thống, giúp phát hiện lỗi nhanh chóng và hiệu quả.

IV. Kết quả nghiên cứu và ứng dụng thực tiễn tại NTTDATA

Nghiên cứu về VDM++ đã mang lại nhiều kết quả tích cực cho hệ thống IMP tại NTTDATA Việt Nam. Việc áp dụng phương pháp này không chỉ giúp cải thiện chất lượng thiết kế mà còn giảm thiểu thời gian phát triển và chi phí.

4.1. Đánh giá hiệu quả của VDM trong dự án IMP

Việc áp dụng VDM++ đã giúp các nhà phát triển nhận diện và khắc phục các lỗi trong giai đoạn thiết kế, từ đó nâng cao chất lượng sản phẩm. Các kết quả cho thấy rằng thời gian phát triển đã giảm đáng kể nhờ vào việc phát hiện lỗi sớm.

4.2. Các bài học rút ra từ việc áp dụng VDM

Các bài học từ việc áp dụng VDM++ cho thấy rằng việc mô hình hóa chính xác và kiểm thử tự động là rất quan trọng. Điều này không chỉ giúp cải thiện quy trình phát triển mà còn đảm bảo rằng sản phẩm cuối cùng đáp ứng được yêu cầu của khách hàng.

V. Kết luận và hướng phát triển tương lai cho VDM

Nghiên cứu về VDM++ cho mô hình hóa và kiểm thử hệ thống IMP tại NTTDATA Việt Nam đã mở ra nhiều cơ hội mới cho việc phát triển phần mềm. Hướng phát triển tương lai sẽ tập trung vào việc cải thiện quy trình mô hình hóa và kiểm thử, từ đó nâng cao chất lượng sản phẩm.

5.1. Tương lai của VDM trong phát triển phần mềm

VDM++ có tiềm năng lớn trong việc cải thiện quy trình phát triển phần mềm. Việc tiếp tục nghiên cứu và phát triển các công cụ hỗ trợ sẽ giúp các nhà phát triển dễ dàng hơn trong việc áp dụng VDM++ vào các dự án thực tế.

5.2. Khuyến nghị cho các nhà phát triển phần mềm

Các nhà phát triển phần mềm nên xem xét việc áp dụng VDM++ trong quy trình phát triển của họ. Việc này không chỉ giúp cải thiện chất lượng sản phẩm mà còn giảm thiểu rủi ro và chi phí phát triển.

Nội dung chính

Tổng quan nghiên cứu

Trong kỹ nghệ phần mềm hiện đại, các số liệu thống kê chỉ ra rằng có khoảng 50% đến 60% tổng số lỗi hệ thống bắt nguồn trực tiếp từ giai đoạn đặc tả yêu cầu và thiết kế chi tiết. Chi phí khắc phục các sai sót này ở giai đoạn bảo trì hoặc kiểm thử tích hợp thường cao gấp 10 đến 100 lần so với việc xử lý ngay từ bước đầu. Tại các doanh nghiệp phát triển phần mềm, điển hình như NTT DATA Vietnam, việc thẩm định chất lượng tài liệu thiết kế chi tiết phần lớn vẫn dựa vào kỹ thuật thủ công thông qua bảng kiểm (checklist) và trực quan của kỹ sư. Cách tiếp cận này bộc lộ hạn chế lớn khi không thể bao quát các trạng thái logic phức tạp, sự không nhất quán giữa các bảng dữ liệu và lỗi tương tác thời gian thực.

Luận văn tập trung nghiên cứu giải pháp ứng dụng phương pháp đặc tả hình thức VDM++ (Vienna Development Method) nhằm mô hình hóa và kiểm thử sớm thiết kế cho hệ thống Quản lý bảo dưỡng công nghiệp (IMP - Industrial Maintenance Program). Nghiên cứu được triển khai thực nghiệm trong năm 2015 tại NTT DATA Vietnam trên nền tảng khung ứng dụng intra-mart. Mục tiêu trọng tâm là thiết lập quy trình kiểm thử mô hình (Modelling Test), phát hiện các lỗi tiềm ẩn trong tài liệu thiết kế trước khi chuyển giao sang giai đoạn lập trình. Ý nghĩa khoa học và thực tiễn của đề tài được khẳng định qua việc cắt giảm hơn 30% khối lượng công việc phải làm lại (rework), nâng cao tính chính xác của tài liệu thiết kế và tối ưu hóa chi phí sản xuất phần mềm theo quy trình chuẩn TeraSS.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Nghiên cứu được xây dựng trên nền tảng phương pháp phát triển Vienna (VDM), một trong những phương pháp hình thức lâu đời bắt nguồn từ phòng thí nghiệm IBM Vienna từ thập niên 1970 và đã được chuẩn hóa qua chuẩn ISO VDM-SL. Luận văn kế thừa và phát triển trên nhánh mở rộng hướng đối tượng VDM++, cho phép mô hình hóa các hệ thống phức tạp thông qua cấu trúc lớp (Class), tính kế thừa và đa hình.

Khung lý thuyết của VDM++ vận hành dựa trên 4 khái niệm nền tảng:

• Biến thể hiện (Instance Variables) kết hợp cùng biểu thức bất biến (Invariants - inv) nhằm thiết lập các ràng buộc logic chặt chẽ cho trạng thái dữ liệu.
• Hàm (Functions) và Phương thức (Operations) được kiểm soát bởi tiền điều kiện (pre) cùng hậu điều kiện (post).
• Ràng buộc đồng bộ (sync) điều khiển luồng thực thi trong môi trường đa luồng phân tán.
• Hệ thống kiểu dữ liệu đa dạng gồm kiểu cơ bản (bool, nat, nat1, real, token, quote) và kiểu khởi tạo cấu trúc (Union, Product, Record, Map, Set, Sequence).

Bên cạnh VDM++, nghiên cứu tích hợp mô hình kiến trúc MVC (Model-View-Controller) trên nền tảng intra-mart framework và quy trình phát triển phần mềm chuẩn TeraSS dựa trên mô hình chữ V gồm 4 giai đoạn của tập đoàn NTT DATA.

Phương pháp nghiên cứu

Nghiên cứu sử dụng phương pháp thực nghiệm kết hợp phân tích đối chiếu trên toàn bộ 100% các phân hệ nghiệp vụ trọng yếu của hệ thống IMP. Cỡ mẫu nghiên cứu bao gồm toàn bộ các thực thể cơ sở dữ liệu quan trọng và 4 cấp độ phê duyệt kế hoạch bảo dưỡng (Kỹ sư, Trưởng phòng, Quản lý chung và Giám đốc điều hành). Phương pháp chọn mẫu có chủ đích (purposive sampling) được lựa chọn nhằm tập trung trực tiếp vào các module có độ phức tạp cao, tần suất phát sinh lỗi lớn như bảng kế hoạch năm (Imp_Schedule_Annual) và chi tiết kế hoạch (Imp_Schedule_Annual_Pln_Detail).

Lý do lựa chọn phương pháp phân tích hình thức thông qua bộ công cụ Overture IDE phiên bản 2.6 phát hành tháng 6 năm 2015 kết hợp với Modelio là nhằm tạo ra khả năng chuyển đổi hai chiều giữa mô hình đồ họa UML và ngôn ngữ toán học VDM++. Phương pháp kiểm thử tổ hợp (Combinatorial Testing - CT) và kiểm tra động (Dynamic Checks) được áp dụng để quét toàn bộ không gian trạng thái, xác thực tính bất biến và các điều kiện biên của hệ thống trong suốt timeline thực hiện dự án năm 2015.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

Quá trình áp dụng quy trình mô hình hóa VDM++ vào dự án IMP đã mang lại những kết quả đo lường cụ thể, chứng minh tính vượt trội so với quy trình thẩm định truyền thống:

• Phát hiện sớm và phân loại chính xác 100% các lỗi tiềm ẩn trong tài liệu thiết kế: Thông qua kiểm thử mô hình (Modelling Test), nghiên cứu đã bóc tách các sai sót thành 3 nhóm ưu tiên rõ rệt. Nhóm ưu tiên cao gồm các lỗi vi phạm tính toàn vẹn dữ liệu khi tạo mới kế hoạch và xung đột quyền hạn duyệt qua 4 cấp. Nhóm ưu tiên trung bình chiếm khoảng 45% tổng số lỗi, chủ yếu liên quan đến sự bất tương thích kiểu dữ liệu giữa SQL Server và VDM. Nhóm ưu tiên thấp liên quan đến tính nhất quán trong quy chuẩn đặt tên biến và cấu trúc hàm dùng chung.
• Tối ưu hóa chu trình chuyển đổi mô hình UML - VDM++: Khả năng tích hợp giữa Modelio và Overture qua chuẩn XMI/UML giúp giảm hơn 40% thời gian xây dựng đặc tả hình thức so với việc lập trình mô hình thủ công từ đầu.
• Nâng cao năng suất lập trình nhờ tự động hóa sinh mã nguồn: Tính năng sinh mã Java tự động từ mô hình VDM++ đã tạo ra bộ khung chuẩn xác, giúp đội ngũ phát triển giảm 25% thời gian viết mã tầng Model và loại bỏ hoàn toàn các lỗi sai lệch logic nghiệp vụ giữa thiết kế và mã nguồn thực thi.

Thảo luận kết quả

Nguyên nhân chính dẫn đến sự cải thiện vượt bậc về chất lượng là do VDM++ đã thay thế việc kiểm tra cảm tính bằng công cụ toán học chính xác. Trình thông dịch của Overture thực thi trực tiếp các kịch bản kiểm thử tổ hợp trên mô hình thiết kế, buộc mọi ràng buộc logic phải thỏa mãn tiền điều kiện và hậu điều kiện trước khi triển khai thực tế.

Dữ liệu so sánh timeline dự án trước và sau khi cải tiến có thể được trình bày rõ ràng qua biểu đồ Gantt và bảng tổng hợp phân loại lỗi. Khi áp dụng quy trình mới, thời gian dành cho giai đoạn phân tích thiết kế tăng khoảng 15%, tuy nhiên thời gian cho giai đoạn lập trình (Coding) và kiểm thử đơn vị (Unit Test) giảm tới 35%, đồng thời giai đoạn kiểm thử tích hợp (IT) giảm 20% do không còn lỗi giao tiếp giữa các module.

Kết quả thực nghiệm tại NTT DATA Vietnam hoàn toàn tương đồng với các công bố khoa học từ cộng đồng nghiên cứu Overture tại Đại học Aarhus (Đan Mạch) và Đại học Newcastle (Anh), khẳng định việc đầu tư công sức vào giai đoạn mô hình hóa sớm luôn mang lại hiệu quả kinh tế cao và bảo đảm an toàn cho các hệ thống phần mềm quy mô lớn.

Đề xuất và khuyến nghị

Nhằm phát huy tối đa hiệu quả của phương pháp đặc tả hình thức VDM++, nghiên cứu đề xuất 4 nhóm giải pháp mang tính chiến lược:

• Chuẩn hóa quy trình cải tiến TeraSS trong doanh nghiệp: Khuyến nghị Ban Giám đốc và Bộ phận Đảm bảo chất lượng (QA) của NTT DATA Vietnam ban hành quy chế bắt buộc áp dụng bước mô hình hóa VDM++ cho tối thiểu 80% các dự án phần mềm có cấu trúc nghiệp vụ phức tạp, hoàn thành áp dụng trong vòng 6 tháng tới.
• Xây dựng bộ quy chuẩn chuyển đổi dữ liệu SQL Server - Java - VDM++: Giao nhóm Kiến trúc sư phần mềm xây dựng tài liệu ánh xạ chuẩn xác giữa các hệ thống kiểu dữ liệu trong quý 4 năm 2015, nhằm loại bỏ triệt để 100% lỗi sai lệch định dạng dữ liệu phát sinh giữa tầng lưu trữ và tầng xử lý nghiệp vụ.
• Tổ chức các chương trình đào tạo nâng cao kỹ năng công nghệ hình thức: Trung tâm đào tạo nội bộ cần phối hợp cùng các chuyên gia mở 3 khóa tập huấn chuyên sâu về công cụ Overture và Modelio cho ít nhất 50 kỹ sư phân tích hệ thống và lập trình viên trong vòng 1 năm.
• Mở rộng phạm vi nghiên cứu sang ngôn ngữ VDM-RT: Giao phòng Nghiên cứu và Phát triển (R&D) thử nghiệm áp dụng VDM-RT trên 2 dự án hệ thống nhúng và thời gian thực phân tán để đánh giá khả năng kiểm soát tài nguyên phần cứng và tính đồng thời đa luồng.

Đối tượng nên tham khảo luận văn

Tài liệu luận văn mang lại giá trị thực tiễn và học thuật cao cho 4 nhóm đối tượng chuyên môn:

• Kỹ sư phân tích hệ thống (System Analysts) và Kỹ sư cầu nối (BrSE): Cung cấp phương pháp luận chuẩn xác để viết tài liệu thiết kế chi tiết không nhập nhằng, dễ dàng chuyển đổi thành mô hình toán học rõ ràng trước khi bàn giao cho đội ngũ phát triển.
• Quản lý dự án (Project Managers) và Chuyên gia QA/QC: Cung cấp khung kiểm soát chất lượng dựa trên mô hình chữ V cải tiến, giúp lập kế hoạch phân bổ thời gian hợp lý và giảm thiểu rủi ro vượt ngân sách dự án.
• Kỹ sư phát triển phần mềm Java và intra-mart: Cung cấp quy trình khai thác tính năng tự động sinh mã từ VDM++ sang Java, hỗ trợ xây dựng tầng kiến trúc Model chuẩn mực và tối ưu hóa thời gian lập trình.
• Giảng viên, nghiên cứu sinh và sinh viên ngành Công nghệ phần mềm: Là tài liệu tham khảo thực tiễn giá trị về việc đưa các phương pháp hình thức (Formal Methods) từ lý thuyết học thuật vào áp dụng thành công trong môi trường sản xuất công nghiệp phần mềm thực tế.

Câu hỏi thường gặp

• Phương pháp VDM++ có làm tăng tổng chi phí và thời gian thực hiện dự án hay không? Không. Mặc dù thời gian thiết kế ban đầu tăng khoảng 15%, nhưng giai đoạn lập trình và kiểm thử giảm tới 35%. Tổng thời gian và chi phí toàn dự án giảm rõ rệt nhờ loại bỏ được hơn 30% khối lượng công việc phải làm lại do lỗi thiết kế.

• Làm thế nào để đồng bộ giữa biểu đồ lớp UML trong Modelio và mô hình VDM++ trong Overture? Hai công cụ trao đổi dữ liệu qua định dạng chuẩn XMI/UML. Kỹ sư thiết kế sơ đồ lớp trên Modelio, xuất ra tệp UML, sau đó sử dụng tính năng UML Transformation trong Overture để chuyển đổi tự động thành các lớp VDM++ tương ứng.

• Vai trò của biểu thức bất biến (Invariant) trong mô hình hóa cơ sở dữ liệu là gì? Biểu thức bất biến (inv) đóng vai trò thiết lập các ràng buộc toàn vẹn dữ liệu ở cấp độ trừu tượng, ví dụ giới hạn miền giá trị trường tuổi từ 0 đến 99 hoặc kiểm tra tính hợp lệ của khóa ngoại trước khi lưu trữ vào bảng dữ liệu.

• Hệ thống IMP đã giải quyết bài toán phức tạp nào thông qua VDM++? Hệ thống đã mô hình hóa thành công luồng phê duyệt kế hoạch bảo dưỡng đa cấp độ gồm 4 bước nghiêm ngặt, đảm bảo tính đúng đắn của dữ liệu chuyển giao giữa Kỹ sư, Trưởng phòng, Quản lý chung và Giám đốc điều hành.

• Overture IDE hỗ trợ kiểm thử thiết kế như thế nào trước khi viết mã nguồn? Overture cung cấp tính năng kiểm tra kiểu động, kiểm tra bất biến, tiền điều kiện, hậu điều kiện và chạy các kịch bản kiểm thử tổ hợp (Combinatorial Testing) trực tiếp trên mô hình để phát hiện lỗi logic ngay trong giao diện gỡ lỗi.

Kết luận

• Luận văn đã hệ thống hóa toàn diện cơ sở lý thuyết về phương pháp đặc tả hình thức VDM++ và bộ công cụ mã nguồn mở Overture IDE 2.6 kết hợp Modelio.
• Phân tích sâu sắc các hạn chế của quy trình thẩm định thiết kế truyền thống tại NTT DATA Vietnam và đề xuất giải pháp cải tiến mô hình chữ V.
• Ứng dụng thành công VDM++ vào việc mô hình hóa cấu trúc dữ liệu SQL Server và luồng nghiệp vụ phê duyệt của hệ thống bảo dưỡng công nghiệp IMP.
• Chứng minh tính hiệu quả thực tế qua việc phát hiện sớm các lỗi thiết kế nghiêm trọng, giảm thiểu 30% chi phí làm lại và rút ngắn 25% thời gian lập trình.
• Đặt nền móng vững chắc cho lộ trình mở rộng ứng dụng VDM-RT trên các hệ thống nhúng trong 12 tháng tiếp theo, mở ra hướng tiếp cận chuẩn mực cho ngành kỹ nghệ phần mềm Việt Nam.

Trích đoạn nội dung tài liệu

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 [e-mail] 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 [e-mail] 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 [e-mail] 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 [e-mail] 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.