Bài giảng Đặc tả hình thức - Chương 1: Tổng quan - Vũ Thanh Nguyên

1Chương 1 Tổng quan Giảng viên: PGS.TS. Vũ Thanh Nguyên Trường Đại học Công Nghệ Thông Tin, ĐHQG-HCM Khoa Công Nghệ Phần Mềm 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 2Mở đầu Mục tiêu và Yêu cầu phần mềm:  Mục tiêu: cái cần hướng tới  Yêu cầu: cái cụ thể mà có thể kiểm tra được 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 3Mở đầu Mục tiêu và Yêu cầu phần mềm:  Yêu cầu chức năng: Mô tả một chức năng (dịch vụ) cụ thể mà phần mềm cung cấp: Mô tả hệ thống sẽ làm gì Mô tả các chức năng hoặc các dịch vụ của hệ thống một cách chi tiết  Yêu cầu phi chức năng: Không đề cập trực tiếp tới các chức năng cụ thể của hệ thống. Đó là các ràng buột về chất lượng, về môi trường, chuẩn sử dụng, qui trình phát triển phần mềm 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 4Mở đầu Mục tiêu và Yêu cầu phần mềm:  Yêu cầu phi chức năng: 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 5Mở đầu Mục tiêu và Yêu cầu phần mềm:  Yêu cầu về sản phẩm: Tốc độ, độ tin cậy, bộ nhớ, giao diện, quy trình tác nghiệp  Yêu cầu về tiến trình phát triển: Các chuẩn, phương pháp thiết kế, ngôn ngữ lập trình  Yêu cầu ngoại lai: Chi phí, thời gian, bản quyền 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 6Đặc tả hình thức và quy trình CNPM Xác định Yêu cầu Phân tích Thiết kế Cài đặt Kiểm chứng Triển khai Khảo sát Hiện trạng Waterfall Các hoạt động trong thế giới thực Các yêu cầu Mô hình Thế giới thực Mô hình phần mềm Phần mềm Phần mềm “chất lượng” 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 7Mở đầu 4/5/2019 PGS.TS. Vũ Thanh Nguyên Quy Trình CuuDuongThanCong.com https://fb.com/tailieudientucntt 8Mở đầu  Những lưu ý:  Phân tích:  Lập các mô hình thế giới thực: Mô hình dữ liệu, Các ràng buộc, Mô hình xử lý, Mô hình trạng thái, Mô hình thời gian, Mô hình không gian. Đặc tả: Các sơ đồ, Các phát biểu về ràng buộc, Các quy định về công thức tính toán, Thiết kế dữ liệu, Các hàm kiểm tra ràng buộc.  Thiết kế:  Lập mô hình phần mềm: Hệ thống dữ liệu, Hệ thống giao diện, Hệ thống xử lý Đặc tả: Các sơ đồ, Các thao tác trên màn hình, Các hàm xử lý, Các hàm. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 9Mở đầu  Những lưu ý:  Kiểm chứng: Kiểm tra tính đúng đắn: Dữ liệu, Hàm, Giao diện. Đặc tả: Kiểm tra tính đúng đắn của hàm.  Ứng dụng của đặc tả:  Mô tả lại các kết quả đã đạt được trong từng giai đoạn của quy trình công nghệ phần mềm. Ứng dụng dạng này thường được sử dụng trong các báo cáo.  Phát sinh kết quả cho giai đoạn kế tiếp dựa vào đặc tả của giai đoạn trước. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 10 Mở đầu  Ngôn ngữ  Ngôn ngữ c n .  Về c bên trong thì ngôn ngữ là một t ng)  p) hay là một t liên quan. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 11 Mở đầu  LỊCH SỬ RA ĐỜI VÀ PHÁT TRIỂN CỦA ĐẶC TẢ HÌNH THỨC  Các kỹ thuật về đặc tả hình thức đã được sử dụng trong ngành Tin học trong suốt hơn 30 năm qua (từ những năm đầu của thập niên 70).  Có rất nhiều mô hình cũng như ngôn ngữ đặc tả được ra đời, mặc dù đa số chúng đều dựa trên cơ sở của toán học.  Các ngôn ngữ đặc tả không hình thức:  Booch, Rumbaugh (thế hệ thứ 1)  UML (thế hệ thứ 2)  OOCL – Object-oriented Change and Learning (thế hệ thứ 3)  Các ngôn ngữ đặc tả hình thức:  OCL, Predicate Calculus, CDM, UNITY, VDM, Z  Object-Z (Z++), VDM++ 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 12 Mở đầu  Các ngôn ngữ đặc tả được thiết kế và ra đời để sử dụng cho nhiều mục đích khác nhau. Các ngôn ngữ này được phân loại theo 3 tiêu chí chính:  Mức độ trừu tượng hoá: Việc đặc tả hệ thống có thể có nhiều mức độ khác nhau.có thể một ngôn ngữ đặc tả chỉ dùng để mô tả các hệ thống tĩnh và nhỏ, nhưng cũng có thể hệ thống cần đặc tả rất to lớn và phức tạp cả về quy mô cũng như hoạt động. Mức độ trừu tượng hoá quyết định một ngôn ngữ đặc tả có thể dùng để mô tả hệ thống nào. Nếu bao quát quá nhiều thứ thì cồng kềnh, nhưng nếu đơn giản quá thì sẽ không có nhiều khả năng ứng dụng. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 13 Mở đầu  Các ngôn ngữ đặc tả được thiết kế và ra đời để sử dụng cho nhiều mục đích khác nhau. Các ngôn ngữ này được phân loại theo 3 tiêu chí chính:  Phạm vi ứng dụng: Mỗi ngôn ngữ đặc tả thường thiết kế nhằm mục đích phục vụ cho một hay một số lĩnh vực cụ thể. Ví dụ: VDM được thiết kế để sử dụng trong thiết kế các mạch số; phép toán mệnh đề được sử dụng trong đặc tả và chứng minh các thuật toán tính toán; UNITY được dùng trong đặc tả và kiểm chứng các hệ thống song song;. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 14 Mở đầu  Các ngôn ngữ đặc tả được thiết kế và ra đời để sử dụng cho nhiều mục đích khác nhau. Các ngôn ngữ này được phân loại theo 3 tiêu chí chính:  Mục đích sử dụng: Một ngôn ngữ đặc tả thường được thiết kế nhằm phục vụ cho một trong hai đối tượng chính là con người và máy tính. Điều khó khăn ở đây là phải làm sao dung hoà được điều nà, vì nếu ngôn ngữ đó gần gũi với ngôn ngữ tự nhiên của con người thì máy tính rất khó phân tích, xử lý và diễn giải; ngược lại, nếu nó quá gần với ngôn ngữ máy tính thì con người gặp khó khăn trong quá trình sử dụng. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 15 Mở đầu  Ngôn ngữ hình thức  Là n c.  Giả sử có một bộ từ vựng ta gọi là alphabet, alphabet ∑ = {a, b} và kí hiệu L là ngôn ngữ. Như vậy, ta có thể định nghĩa một số ngôn ngữ trên alphabet ∑ như sau: L1 = {aa, aaa}, L2 = {aba, aab}, L2 = {aba, aab}, L3 = {ab, ba, aabb,..., aaabbb,...} 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 16 Mở đầu  Mô tả và Đặc tả  Mô tả là t ..  Đặc tả là mô tả ngắn gọn, chính xác vấn đề nào đó. Một đặc tả của hệ thống phải ngắn hơn so với cài đặt tương ứng Đặc tả bao gồm 3 loại chính:  Đặc tả phi hình thức (informal) là dạng đặc tả bằng ngôn ngữ tự nhiên tự do, ngôn ngữ tự nhiên có cấu trúc hay bằng các ký hiệu đồ họa.  Đặc tả nửa hình thức (semi-informal) là dạng đặc tả trộn lẫn giữa các ký hiệu toán học, ngôn ngữ tự nhiên và các ký hiệu đồ họa.  . Một số ngôn ngữ hình thức được sử dụng hiện nay như VDM-SL, Z, RSL, Act One, Clear, CCS, CSP, Real-Time Logic, Deontic Logics. Và ngôn ngữ được sử dụng phổ biến để đặc tả hình thức là VDM-SL và Z. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 17 Mở đầu  Quan tâm đến kết quả thực hiện & chuyển giao giữa các giao đoạn. Ngôn ngữ tự nhiên Sơ đồ Độ chính xác không cao, có thể gây ra hiểu nhầm, Dài dòng nếu mô tả đầy đủ. Thích hợp cho việc mô tả chi tiết Độ chính xác tăng lên Trình bày ngắn gọn, trực quan Phù hợp cho việc mô tả 1 cách tổng quát 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 18 Mở đầu  Phương pháp hình thức được chấp nhận ở cả 2 lãnh vực là nghiên cứu và công nghiệp như một con đường có thể giúp đỡ cải tiến chất lượng của 2 hệ thống phần cứng và phần mềm.  Phương pháp hình thức là chìa khóa được sử dụng trong xây dựng các hệ thống phần mềm quan trọng. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 19 Mở đầu  Đặc tả hình thức là sự miêu tả đơn giản của một hệ thống sử dụng các ký hiệu toán học.  Ưu điểm của việc sử dụng toán học chính là nó là sự chính xác, không giống như ngôn ngữ tự nhiên mơ hồ và sơ đồ mà nó thường được sử dụng cho đặc tả.  Nhược điểm của nó là sự bao vây của các ký hiệu vì rất nhiều người hiểu ngôn ngữ tự nhiên hơn toán học  Ngôn ngữ đặc tả cần phải được nghiên cứu và nó được sử dụng như một công cụ thiết kế và nếu ký hiệu được sử dụng đầy đử, nó được xem như công cụ tài liệu hoá. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 20 Mở đầu  Các quá trình thực tế của thiết kế một hệ thống có lẻ bảo đảm sử dụng ký hiệu hình thức liên kết ý tưởng với các thành viên của đội ngũ thiết kế. Một khi thiết kế đã hoàn thành, nó có thể khi đó tạo thành phần cơ bản đối với sự thiết kế bằng tay của hệ thống. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 21 Mở đầu  Tại Sao Sử Dụng Đặc Tả Hình Thức  Đặc tả hình thức là sự rõ ràng và chính xác  Nếu đặc tả hình thức không rõ ràng, nó dễ dàng bảo ở đâu nó bị sai (không rõ ràng) và chỉnh sửa nó.  Nếu không phải là đặc tả hình thức, nó rất khó tìm ra lỗi và chỉnh sứa nó. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 22 Mở đầu  Sử dụng ký hiệu hình thức tăng cường sự hiểu biết của sự vận hành hệ thống, đặc biệt dễ dàng trong thiết kế.  Nó giúp đỡ tổ chức ý tưởng của người thiết kế, tạo sự rõ ràng, thiết kế đơn giản.  Có thể lập luận hình thức về hệ thống bởi những phát biểu và chứng minh định lý về nó.  Nó cung cấp sự kiểm tra rằng hệ thống sẽ được hoạt động như sự thể hiện bởi sự thiết kế. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 23 Mở đầu  Sử dụng các phương pháp hình thức co thể giúp đỡ thăm dò sử lựa chọn thiết kế.  Sử dụng các phương pháp không hình thức, nó dễ dàng che đậy các chi tiết trong giai đoạn thực hiện  Một trong các lợi ích khác của khi sử dụng đặc tả hình thức khác là giá thành sản phẩm sẽ giảm: lỗi phát hiện được chỉnh sửa ở bước thiết kế có thể giảm đi gấp đôi chi phí nếu được phát hiện sau. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 24 Mở đầu  Nhược điểm của việc sử dụng phương pháp hình thức trên ký hiệu toán học, mà có lẻ nó chứa đựng các ký tự xa lạ mà yêu cầu các nhà thiết kế chú tâm đến các khoá huấn luyện.  Tuy nhiên nếu so sánh việc nghiên cứu một ngôn ngữ lập trình mới, thì việc học ký hiệu sẽ tốn ít thời gian hơn và dễ hơn. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 25 Ví dụ: Phát biểu RBTV trong CSDL  Ví dụ (R1)  Ngôn ngữ tự nhiên  Mức lương của một người nhân viên không được vượt quá trưởng phòng  Ngôn ngữ hình thức t  NHANVIEN ( u  PHONGBAN ( v  NHANVIEN ( u.TRPHG  v.MANV  u.MAPHG  t.PHG  t.LUONG  v.LUONG ))) 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 26 Ví dụ: Phát biểu RBTV trong CSDL  Ví dụ (R2)  Ngôn ngữ tự nhiên  Người quản lý trực tiếp phải là một nhân viên trong công ty  Ngôn ngữ hình thức t  NHANVIEN ( t.MA_NQL  null  s  NHANVIEN (t.MA_NQL  s.MANV )) 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 27 Vai trò đặc tả hình thức trong quá trình phát triển phần mềm  Trong phát triển phần mềm thì đặc tả định nghĩa một hệ thống, một module chương trình hay một sản phẩm cần phải làm cái gì, tuy nhiên không cần thiết mô tả nó phải làm thế nào hay nói cách khác chúng ta chỉ cần mô tả những tính chất của vấn đề đặt ra mà không cần mô tả những tính chất của giải pháp của vấn đề đó. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 28 Vai trò đặc tả hình thức trong quá trình phát triển phần mềm  Đặc tả còn là các hoạt động được tiến hành trong các giai đoạn khác nhau của một tiến trình phần mềm như:  Đặc tả yêu cầu : để tạo sự thống nhất giữa người thiết kế và người sử dụng  Đặc tả kiến trúc hệ thống : để tạo sự thống nhất giữa những người thiết kế và những người cài đặt  Đặc tả modun : nhằm mục đích tạo sự thống nhất giữa những người cài đặt module và người cài đặt sử dụng module này.  Đặc tả hiệu năng và chi phí : là loại đặc tả giúp kiểm tra được hiệu năng thực thi và chi phí xây dựng của phần mềm. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 29 Vai trò đặc tả hình thức trong quá trình phát triển phần mềm  Cách thức nâng cao chất lượng của phần phềm là thay đổi phương pháp xây dựng các đặc tả phần mềm trong các bước thiết kế, trong suốt quá trình phát triển và sau khi triển khai sản phẩm.  Có nhiều phương pháp xây dựng các tài liệu được đưa ra để hỗ trợ xây dựng một hàng loạt các văn bản, hình ảnh, và biểu đồ, tuy nhiên những sản phẩm này thường không chính xác và nhập nhằng ngữ nghĩa.  Đặc tả được sử dụng trong quá trình phát triển hệ thống là đặc tả hình thức. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 30 Vai trò đặc tả hình thức trong quá trình phát triển phần mềm  Gần như là việc sử dụng phương pháp hình thức sẽ trở thành một chuẩn trong quá trình phát triển phần mềm.  Nền tảng toán học được áp dụng khác biệt trong công nghệ cơ khí hay các công nghệ khác, suy cho cùng chúng đều có chung một mục đích là tăng độ chính xác và giúp người sử dụng hiểu và giải thích được các vấn đề xung quanh bảng thiết kế.  Bất cứ lĩnh vực nào, áp dụng toán học vào rất tốn chi phí tuy nhiên xem xét toàn bộ quá trình xây dựng hệ thống thì tổng chi phí giảm đi đáng kể. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 31 Nguyên nhân đặc tả được áp dụng trong các bước của quy trình phát triển phần mềm  Hợp đồng: Chúng ta cần sự thống nhất giữa người sử dụng và người phát triển sản phẩm.  Hợp thức hóa: Sản phẩm làm ra phải đảm bảo chất lượng và mong muốn bởi người sử dụng.  Phục vụ cho quá trình trao đổi giữa người sử dụng và người phát triển sản phẩm hay giữa các người phát triển sản phẩm.  Nhờ các bản đặc tả có thể giúp chúng ta tái sử dụng được các module, chương trình ... 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 32 Ng  ng:  .  c bên trong:  ng).  p).  liên quan.  :  p, ...  y, ...  o, ...  p), ... 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 33 Ng c:  Khái niệm:  c. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 34 Ng  :  .  :  c.  c:  c.  . 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 35 Một số ngôn ngữ đặc tả hình thức Một ngôn ngữ đặc tả hình thức là một ngôn ngữ hình thức dùng để đặc tả mô hình của hệ thống tính toán. VDM-SL Z RSL Act One Clear CCS CSP Real-Time Logic Deontic Logics 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 36 Đặc tả và công nghệ phần mềm  Các giai đoạn trong qui trình công nghệ:  Xác định yêu cầu.  Phân tích.  Thiết kế.  Thực hiện.  Kiểm chứng. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 37 Đặc tả và công nghệ phần mềm Ví dụ 1:  Ngữ cảnh:  Xét đề án phần mềm bài tập toán lớp 5 với:  A: Nhân viên phụ trách thiết kế.  B: Nhân viên lập trình.  C: Nhân viên phụ trách kiểm tra.  A yêu cầu  B “viết hàm xử lí nhập (có kiểm tra tính hợp lệ) của một phân số dưới dạng chuỗi”.  C “kiểm tra và cho đánh giá về hàm xử lí nhập của B trên chuỗi phân số”.  Giả sử không xét đến thông tin về hàm xử lí mà chỉ quan tâm thông tin về “phân số dạng chuỗi” / “chuỗi phân số”. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 38 Đặc tả và công nghệ phần mềm  Ví dụ 2: Tương tự ví dụ 1 với:  Phần mềm bài tập toán cao cấp.  Yêu cầu liên quan đến các hàm xử lí trên số phức (chỉ quan tâm đến nhập liệu dạng chuẩn).  Đóng vai trò của A đặc tả cấu trúc thông tin về số phức (giả sử B, C chưa có khái niệm về số phức). 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 39 Ví dụ Minh họa cho đặc tả kiểu cấu trúc cơ bản: Khai báo cấu trúc HOCSINH gồm họ tên học sinh(kiểu chuỗi), Năm sinh(kiểu số tự nhiên) và điểm trung bình(kiểu số thực). K HOCSINH HoTen : S NamSinh : N DTB : Z 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 40 Ví dụ  Khai báo cấu trúc LOPHOC gồm tên lớp(kiểu chuỗi), sỉ số lớp(kiểu số tự nhiên) và Danh sách học sinh tối đa 50 học sinh (kiểu mảng) K LOPHOC TenLop : S Siso: N DanhSach: M HOCSINH[50] 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 41 Ví dụ  Kiểm tra học sinh nào đó có phải tên đó không với điều kiện nhập là học sinh đó sinh sau năm 1982. H KiemTraTenHocSinh2 (Hs : HOCSINH, Ten : S) Kq : B DKN (Hs.Nm>=1982) KQX ((Kq=true) & (Hs.HoTen = Ten)) |((Kq=false) & (Hs.HoTen!= Ten)) 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt